diff --git a/examples/publications/2020/permutations/evenPhase.pvl b/examples/archive/known-problems/1230/evenPhase.pvl similarity index 100% rename from examples/publications/2020/permutations/evenPhase.pvl rename to examples/archive/known-problems/1230/evenPhase.pvl diff --git a/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/TTTmsg-generatedImplementation.pvl b/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/TTTmsg-generatedImplementation.pvl deleted file mode 100644 index d883452b40..0000000000 --- a/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/TTTmsg-generatedImplementation.pvl +++ /dev/null @@ -1,256 +0,0 @@ -/* -This version is based on tic-tac-toe-board6. - -It tries to get rid of the returneeToken by "just" sending a game end message. This message is used to unequally/asymmetrically, _but_ deterministically, distribute the permissions. Because the permissions are deterministically distributed, it is trivial to prove that full permission to the boards is regained after termination of both threads. - -Interesting: two channels are needed for one game end message, even though we will only use _one_ of them _once_. -*/ - -lock_invariant channelAnnotations(); -class MoveChannel { - boolean transfering; - Move exchangeValue; - Player s,r; // Sending, receiving player - - - inline resource channelAnnotations() = true - ** Perm(transfering, 1) ** Perm(exchangeValue, 1) - ** Perm(s, 1\2) ** s != null - ** Perm(r, 1\2) ** r != null - ** (transfering ==> true - ** exchangeValue.movePerm() - ** ([1\2]s.boardPerm()) - ** ([1\2]r.boardPerm()) - ** s.oneMoveAheadOf(exchangeValue, r) - ) - ; - - requires s != null ** r != null; - ensures committed(this); - ensures Perm(this.s, 1\2) ** Perm(this.r, 1\2); - ensures this.s == s ** this.r == r; - constructor(Player s, Player r) { - transfering = false; - this.s = s; - this.r = r; - commit this; - } - - context_everywhere committed(this); - context Perm(s, 1\8) ** Perm(r, 1\8); - requires v.movePerm(); - requires [1\2]s.boardPerm(); - requires [1\2]r.boardPerm(); - requires s.oneMoveAheadOf(v, r); - void writeValue(Move v) { - lock this; - loop_invariant held(this); - loop_invariant channelAnnotations(); - while(!transfering) { - wait this; - } - transfering = true; - exchangeValue = v; - unlock this; - } - - context_everywhere committed(this); - context Perm(s, 1\8) ** Perm(r, 1\8); - ensures \result.movePerm(); - ensures [1\2]s.boardPerm(); - ensures [1\2]r.boardPerm(); - ensures s.oneMoveAheadOf(\result, r); - Move readValue(){ - lock this; - loop_invariant held(this); - loop_invariant channelAnnotations(); - while(!transfering){ - wait this; - } - Move v = exchangeValue; - transfering = false; - unlock this; - return v; - } - -} - -lock_invariant channelAnnotations(); -class GameEndChannel { - boolean transfering; - int exchangeValue; - Player s,r; // Sending, receiving player - - inline resource channelAnnotations() = true - ** Perm(transfering, 1) ** Perm(exchangeValue, 1) - ** Perm(s, 1\2) ** s != null - ** Perm(r, 1\2) ** r != null - ** (transfering ==> true - ** exchangeValue == 0 // We can only send a meaningless value - ** ([3\4]s.boardPerm()) - ** ([1\4]r.boardPerm()) - ** s.equalBoard(r) - ) - ; - - requires s != null ** r != null; - ensures committed(this); - ensures Perm(this.s, 1\2) ** Perm(this.r, 1\2); - ensures this.s == s ** this.r == r; - constructor(Player s, Player r) { - transfering = false; - this.s = s; - this.r = r; - commit this; - } - - context_everywhere committed(this); - context Perm(s, 1\8) ** Perm(r, 1\8); - requires [1\4]s.boardPerm(); - requires [1\4]r.boardPerm(); - requires s.equalBoard(r); - requires v == 0; - void writeValue(int v) { - lock this; - loop_invariant held(this); - loop_invariant channelAnnotations(); - while(!transfering) { - wait this; - } - transfering = true; - exchangeValue = v; - unlock this; - } - - context Perm(s, 1\8) ** Perm(r, 1\8); - requires committed(this); - ensures [1\4]s.boardPerm(); - ensures [1\4]r.boardPerm(); - ensures s.equalBoard(r); - ensures \result == 0; - int readValue(){ - lock this; - loop_invariant held(this); - loop_invariant channelAnnotations(); - while(!transfering){ - wait this; - } - int v = exchangeValue; - transfering = false; - unlock this; - return v; - } - -} - -class PlayerThread { - - Player p; - Player other; - MoveChannel writeMoveChan; - MoveChannel readMoveChan; - GameEndChannel writeGameEndChan; - GameEndChannel readGameEndChan; - - requires token == 0 || token == 1; - ensures idle(this); - ensures threadPerm(); - ensures ([1\2]p.boardPerm()); - ensures p.emptyBoard(); - ensures p.myToken == token; - ensures p.turn == turn; - ensures Perm(other, 1\2); - ensures Perm(p, 1\2); - ensures Perm(p.myToken, 1\2); - constructor(int token, boolean turn) { - p = new Player(token, turn); - } - - inline resource threadPerm() = true - ** Perm(p, 1\2) ** ([1\2]p.boardPerm()) - ** Perm(p.move, write) ** Perm(p.turn, write) ** Perm(other, 1\2) - ** Perm(p.myToken, 1\2) ** (p.myToken == 0 || p.myToken == 1) - ** Perm(writeMoveChan, write) ** Perm(readMoveChan, write) - ** Perm(writeGameEndChan, write) ** Perm(readGameEndChan, write) - ; - - inline resource chanPerm() = true - ** Perm(writeMoveChan.s, 1\4) ** Perm(writeMoveChan.r, 1\4) - ** Perm(readMoveChan.s, 1\4) ** Perm(readMoveChan.r, 1\4) - ** Perm(writeGameEndChan.s, 1\4) ** Perm(writeGameEndChan.r, 1\4) - ** Perm(readGameEndChan.s, 1\4) ** Perm(readGameEndChan.r, 1\4) - ** committed(writeMoveChan) ** committed(readMoveChan) ** committed(writeGameEndChan) ** committed(readGameEndChan) - ** writeMoveChan.s == this.p ** readMoveChan.r == this.p ** writeGameEndChan.s == this.p ** readGameEndChan.r == this.p - ** writeMoveChan.r == other ** readMoveChan.s == other ** writeGameEndChan.r == other ** readGameEndChan.s == other - ; - - inline resource turnPerm() = true - ** ([1\2]p.boardPerm()) ** ([1\2]other.boardPerm()) - ** p.equalBoard(other) - ; - - context threadPerm() ** chanPerm(); - requires p.emptyBoard(); - requires p.turn ==> turnPerm(); - ensures p.gameFinished(); - ensures ([1\4]p.boardPerm()) ** ([1\4]other.boardPerm()) ** p.equalBoard(other); - run { - loop_invariant threadPerm() ** chanPerm(); - loop_invariant p.turn && !p.gameFinished() ==> turnPerm(); - loop_invariant p.turn && p.gameFinished() ==> turnPerm(); - while (!p.gameFinished()) { - if (p.turn) { - p.createNewMove(); - p.doMove(); - writeMoveChan.writeValue(p.move.copy()); - } else { - p.move = readMoveChan.readValue(); - p.doMove(); - } - p.turn = !p.turn; - } - - if (p.turn) { - writeGameEndChan.writeValue(0); - } else { - readGameEndChan.readValue(); - } - - assert ([3\4]p.boardPerm()) ** ([1\4]other.boardPerm()) ** p.equalBoard(other); - } -} - -void mainFJ() { - PlayerThread p1 = new PlayerThread(0,true); - PlayerThread p2 = new PlayerThread(1,false); - - p1.other = p2.p; - p2.other = p1.p; - - MoveChannel p1p2MoveChan = new MoveChannel(p1.p, p2.p); - MoveChannel p2p1MoveChan = new MoveChannel(p2.p, p1.p); - - p1.writeMoveChan = p1p2MoveChan; - p1.readMoveChan = p2p1MoveChan; - p2.writeMoveChan = p2p1MoveChan; - p2.readMoveChan = p1p2MoveChan; - - GameEndChannel p1p2GameEndChan = new GameEndChannel(p1.p, p2.p); - GameEndChannel p2p1GameEndChan = new GameEndChannel(p2.p, p1.p); - - p1.writeGameEndChan = p1p2GameEndChan; - p1.readGameEndChan = p2p1GameEndChan; - p2.writeGameEndChan = p2p1GameEndChan; - p2.readGameEndChan = p1p2GameEndChan; - - fork p1; - fork p2; - join p1; - join p2; - - // Yay! - assert true - ** p1.p.boardPerm() ** p2.p.boardPerm() - ** p1.p.equalBoard(p2.p) - ; -} diff --git a/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/TTTlast-generated.pvl b/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/TTTlast-generated.pvl deleted file mode 100644 index 8843ccbcec..0000000000 --- a/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/TTTlast-generated.pvl +++ /dev/null @@ -1,177 +0,0 @@ -class MoveChannel { - boolean transfering; - Move exchangeValue; - Player s,r; // Sending, receiving player - - resource lock_invariant() = channelAnnotations(); - - inline resource channelAnnotations() = true - ** Perm(transfering, 1) ** Perm(exchangeValue, 1) - ** Perm(s, 1\2) ** s != null - ** Perm(r, 1\2) ** r != null - ** (transfering ==> true - ** exchangeValue.movePerm() - ** ([1\2]s.boardPerm()) - ** ([1\2]r.boardPerm()) - ** s.oneMoveAheadOf(exchangeValue, r) - ** ([1\2]s.returneeBound(r)) - ** ([1\2]s.returneeToken()) - ** (!s.gameFinished() ==> ([1\2]s.returneeToken())) - ) - ; - - requires s != null ** r != null; - ensures Perm(this.s, 1\2) ** Perm(this.r, 1\2); - ensures this.s == s ** this.r == r; - MoveChannel(Player s, Player r) { - transfering = false; - this.s = s; - this.r = r; - } - - context Perm(s, 1\8) ** Perm(r, 1\8); - requires v.movePerm(); - requires [1\2]s.boardPerm(); - requires [1\2]r.boardPerm(); - requires s.oneMoveAheadOf(v, r); - requires ([1\2]s.returneeBound(r)); - requires ([1\2]s.returneeToken()); - requires !s.gameFinished() ==> ([1\2]s.returneeToken()); - void writeValue(Move v) { - lock this; - loop_invariant held(this); - loop_invariant channelAnnotations(); - while(!transfering) { - wait this; - } - transfering = true; - exchangeValue = v; - unlock this; - } - - context Perm(s, 1\8) ** Perm(r, 1\8); - ensures \result.movePerm(); - ensures [1\2]s.boardPerm(); - ensures [1\2]r.boardPerm(); - ensures s.oneMoveAheadOf(\result, r); - ensures ([1\2]s.returneeBound(r)); - ensures ([1\2]s.returneeToken()); - ensures !s.gameFinished() ==> ([1\2]s.returneeToken()); - Move readValue(){ - lock this; - loop_invariant held(this); - loop_invariant channelAnnotations(); - while(!transfering){ - wait this; - } - Move v = exchangeValue; - transfering = false; - unlock this; - return v; - } - -} - -class PlayerThread { - - Player p; - Player other; - MoveChannel writeMoveChan; - MoveChannel readMoveChan; - - requires token == 0 || token == 1; - ensures threadPerm(); - ensures ([1\2]p.boardPerm()); - ensures p.emptyBoard(); - ensures p.myToken == token; - ensures p.turn == turn; - ensures Perm(p.returnee, 1); - ensures Perm(other, 1\2); - ensures Perm(p, 1\2); - ensures Perm(p.myToken, 1\2); - PlayerThread(int token, boolean turn) { - p = new Player(token, turn); - } - - inline resource threadPerm() = true - ** Perm(p, 1\2) ** ([1\2]p.boardPerm()) - ** Perm(p.move, write) ** Perm(p.turn, write) ** Perm(other, 1\2) - ** Perm(p.myToken, 1\2) ** (p.myToken == 0 || p.myToken == 1) - ** Perm(writeMoveChan, write) ** Perm(readMoveChan, write) - ; - - inline resource chanPerm() = true - ** Perm(writeMoveChan.s, 1\4) ** Perm(writeMoveChan.r, 1\4) - ** Perm(readMoveChan.s, 1\4) ** Perm(readMoveChan.r, 1\4) - ** writeMoveChan.s == this.p ** readMoveChan.r == this.p - ** other == writeMoveChan.r ** writeMoveChan.r == readMoveChan.s - ; - - inline resource turnPerm() = true - ** ([1\2]p.boardPerm()) ** ([1\2]other.boardPerm()) - ** p.equalBoard(other) - ; - - context threadPerm() ** chanPerm(); - requires p.emptyBoard(); - context [1\4]p.returneeBound(other); - requires p.turn ==> turnPerm() ** ([1\2]p.returneeBound(other)) ** p.returneeToken(); - ensures p.gameFinished(); - ensures (([1\2]p.returneeToken()) ** (p.returnee.token == p.myToken ==> turnPerm())); - void run() { - loop_invariant threadPerm() ** chanPerm(); - loop_invariant [1\4]p.returneeBound(other); - loop_invariant p.turn && !p.gameFinished() ==> - turnPerm() - ** ([1\2]p.returneeBound(other)) - ** p.returneeToken(); - loop_invariant p.gameFinished() ==> - (([1\2]p.returneeToken()) ** - (p.returnee.token == p.myToken ==> turnPerm())); - while (!p.gameFinished()) /* decreases */ { - // int x = p.fieldSize() - p.countMoves() - if (p.turn) { - p.createNewMove(); - p.doMove(); - if (p.gameFinished()) { - p.returnee.token = 1 - p.myToken; - } - writeMoveChan.writeValue(p.move.copy()); - } else { - p.move = readMoveChan.readValue(); - p.doMove(); - } - // assert x > p.fieldSize() - p.countMoves(); - p.turn = !p.turn; - } - } -} - -class MainFJ { - static void mainFJ() { - PlayerThread p1 = new PlayerThread(0,true); - PlayerThread p2 = new PlayerThread(1,false); - - p1.other = p2.p; - p2.other = p1.p; - - p1.p.returnee = new Returnee(); - p2.p.returnee = p1.p.returnee; - p1.p.returnee.token = 0; - - MoveChannel p1p2MoveChan = new MoveChannel(p1.p, p2.p); - MoveChannel p2p1MoveChan = new MoveChannel(p2.p, p1.p); - - p1.writeMoveChan = p1p2MoveChan; - p1.readMoveChan = p2p1MoveChan; - p2.writeMoveChan = p2p1MoveChan; - p2.readMoveChan = p1p2MoveChan; - - fork p1; - fork p2; - join p1; - join p2; - - assert p1.p.equalBoard(p2.p); - } -} diff --git a/examples/publications/2023/FM2023VeyMont/paper-examples/veymont-swap.pvl b/examples/publications/2023/FM2023VeyMont/paper-examples/veymont-swap.pvl index 7925e0fcfd..8623928178 100644 --- a/examples/publications/2023/FM2023VeyMont/paper-examples/veymont-swap.pvl +++ b/examples/publications/2023/FM2023VeyMont/paper-examples/veymont-swap.pvl @@ -26,9 +26,9 @@ choreography Swap(int x, int y) { alex.temp := alex.v; bobby.temp := bobby.v; // Then send them to the other - channel_invariant Perm(bobby.oldV, read) ** \msg == bobby.oldV; + channel_invariant Perm(\sender.oldV, read) ** \msg == \sender.oldV; communicate alex.v <- bobby.temp; - channel_invariant Perm(alex.oldV, read) ** \msg == alex.oldV; + channel_invariant Perm(\sender.oldV, read) ** \msg == \sender.oldV; communicate bobby.v <- alex.temp; } } diff --git a/examples/concepts/veymont/FM2024 - VeyMont/0-TTT/TTT.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/0-TTT.pvl similarity index 79% rename from examples/concepts/veymont/FM2024 - VeyMont/0-TTT/TTT.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/0-TTT.pvl index 46e7b48bed..27bd18dae1 100644 --- a/examples/concepts/veymont/FM2024 - VeyMont/0-TTT/TTT.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/0-TTT.pvl @@ -1,7 +1,7 @@ inline resource ticTacToeAnnotations(Player p1, Player p2) = - p1.myMark == 0 ** p2.myMark == 1 - ** p1.turn != p2.turn - ** p1.equalBoard(p2); + p1.myMark == 0 ** p2.myMark == 1 ** + p1.turn != p2.turn ** + p1.equalBoard(p2); choreography TTT() { endpoint p1 = Player(0, true); @@ -11,6 +11,7 @@ choreography TTT() { ensures (\chor p1.gameFinished() && p2.gameFinished()); run { loop_invariant (\chor ticTacToeAnnotations(p1, p2)); + loop_invariant p1.myMark == 0 ** p2.myMark == 1; while(!p1.gameFinished() && !p2.gameFinished()) { if(p1.turn && !p2.turn) { p1.createNewMove(); @@ -18,14 +19,14 @@ choreography TTT() { (\chor \msg.i == \sender.move.i ** \msg.j == \sender.move.j ** \msg.mark == \sender.move.mark); - communicate p2.move <- p1.move.clone(); + communicate p2.move <- p1.move.copy(); } else { p2.createNewMove(); channel_invariant (\chor \msg.i == \sender.move.i ** \msg.j == \sender.move.j ** \msg.mark == \sender.move.mark); - communicate p1.move <- p2.move.clone(); + communicate p1.move <- p2.move.copy(); } p1.doMove(); p2.doMove(); diff --git a/examples/concepts/veymont/FM2024 - VeyMont/0-TTT/Move.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/Move.pvl similarity index 95% rename from examples/concepts/veymont/FM2024 - VeyMont/0-TTT/Move.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/Move.pvl index 40a34e5741..993f587517 100644 --- a/examples/concepts/veymont/FM2024 - VeyMont/0-TTT/Move.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/Move.pvl @@ -10,7 +10,7 @@ class Move { ensures \result.i == i ** \result.j == j ** \result.mark == mark; ensures i == \old(i) ** j == \old(j) ** mark == \old(mark); - Move clone() { + Move copy() { return new Move(i, j, mark); } } diff --git a/examples/concepts/veymont/FM2024 - VeyMont/0-TTT/Player.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/Player.pvl similarity index 100% rename from examples/concepts/veymont/FM2024 - VeyMont/0-TTT/Player.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/Player.pvl diff --git a/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/1-TTTmsg.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl similarity index 85% rename from examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/1-TTTmsg.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl index e61fa7f154..4845eff1d5 100644 --- a/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/1-TTTmsg.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl @@ -5,7 +5,6 @@ inline resource turnInvariant(Player p, Player q) = ; inline resource state(Player p, boolean withBoardPerm) = - // TODO: refactor boardPerm to simply state? (withBoardPerm ==> ([1\2]p.boardPerm())) ** Perm(p.move, 1) ** p.move != null ** p.move.state() ** Perm(p.temp, 1) ** Perm(p.turn, 1) ** Perm(p.myMark, 1); @@ -14,14 +13,13 @@ choreography Main() { endpoint p1 = Player(0, true); endpoint p2 = Player(1, false); - // TODO: If inline predicates were not removed here already, inference could also detect boardPerm is p1/p2's. requires (\endpoint p1; state(p1, true)); requires (\endpoint p2; state(p2, true)); - ensures (\endpoint p1; state(p1, false)); // TODO: remove (also param) + ensures (\endpoint p1; state(p1, false)); ensures (\endpoint p2; state(p2, false)); requires (\endpoint p1; p1.turn ==> turnInvariant(p1, p2)); requires (\endpoint p2; p2.turn ==> turnInvariant(p2, p1)); - // TODO: endpoint annotations can be removed here if we switch to more lightweight encoding + // Endpoint annotations using "\endpoint" will be removed after switching to the lightweight encoding. requires (\chor (\endpoint p1; p1.turn) != (\endpoint p2; p2.turn)); requires p1.emptyBoard() ** p2.emptyBoard(); ensures (\endpoint p1; @@ -32,8 +30,7 @@ choreography Main() { ([3\4]p2.boardPerm()) ** ([1\4]p1.boardPerm()) ** p2.equalBoard(p1)); - // TODO: Would like this as well. Probably will work with the lightweight encoding - ensures p1.gameFinished() && p2.gameFinished(); + ensures p1.gameFinished() && p2.gameFinished(); run { loop_invariant (\endpoint p1; state(p1, true)) ** (\endpoint p2; state(p2, true)); loop_invariant (\endpoint p1; p1.turn ==> turnInvariant(p1, p2)); @@ -63,7 +60,7 @@ choreography Main() { p1.turn := !p1.turn; p2.turn := !p2.turn; - // TODO: Remove when lightweight encoding + // Assumption required for shortcoming in one of the backends. The the other backend can verify it just fine. Can be removed after implementing the lightweight encoding. assume (\chor (\endpoint p1; p1.gameFinished()) == (\endpoint p2; p2.gameFinished())); } assume (\chor (\endpoint p1; p1.gameFinished()) == (\endpoint p2; p2.gameFinished())); @@ -84,5 +81,8 @@ choreography Main() { \receiver.equalBoard(\sender); communicate p1.temp <- p2: true; } + + p1.finish(); + p2.finish(); } } diff --git a/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/Move.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/Move.pvl similarity index 100% rename from examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/Move.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/Move.pvl diff --git a/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/Player.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/Player.pvl similarity index 98% rename from examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/Player.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/Player.pvl index 453e5c2c83..de155ff91a 100644 --- a/examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/Player.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/Player.pvl @@ -141,6 +141,8 @@ class Player { ensures readMoveCell(move,this) == -1; void createNewMove(); + // Hook for the test suite to replace code + void finish() { } } requires Perm(move.i, read) ** Perm(move.j, read); diff --git a/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/2-TTTlast.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl similarity index 86% rename from examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/2-TTTlast.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl index 24dffeb206..4ec2b2e43a 100644 --- a/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/2-TTTlast.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl @@ -5,7 +5,6 @@ inline resource turnInvariant(Player p, Player q) = ; inline resource state(Player p, Player other, boolean withBoardPerm) = - // TODO: refactor boardPerm to simply state? (withBoardPerm ==> ([1\2]p.boardPerm())) ** Perm(p.move, 1) ** p.move != null ** p.move.state() ** Perm(p.turn, 1) ** Perm(p.myMark, 1\2) ** (p.myMark == 0 || p.myMark == 1) ** @@ -21,10 +20,10 @@ choreography Main() { turnInvariant(p1, p2) ** ([1\2]p1.returnerBound(p2)) ** p1.returnerMark()); requires (\endpoint p2; p2.turn ==> turnInvariant(p1, p2) ** ([1\2]p2.returnerBound(p1)) ** p2.returnerMark()); + // Endpoint annotations using "\endpoint" will be removed after switching to the lightweight encoding. requires (\chor (\endpoint p1; p1.turn) != (\endpoint p2; p2.turn)); ensures (\endpoint p1; state(p1, p2, true)) ** (\endpoint p2; state(p2, p1, true)); - // TODO: Would like to have - // ensures p1.gameFinished() && p2.gameFinished(); + ensures p1.gameFinished() && p2.gameFinished(); ensures (\endpoint p1; ([1\2]p1.returnerMark()) ** (p1.returner.mark == p1.myMark ==> turnInvariant(p1, p2))); ensures (\endpoint p2; ([1\2]p2.returnerMark()) ** @@ -63,12 +62,7 @@ choreography Main() { (!\sender.gameFinished() ==> ([1\2]\sender.returnerMark())); communicate p2.move <- p1.move.copy(); p2.doMove(); - assert (\chor (\endpoint p2; p2.gameFinished() && p2.returner.mark == p2.myMark ==> turnInvariant(p2, p1))); - assert (\chor (\endpoint p1; p1.gameFinished() ==> p1.returner.mark != p1.myMark)); - assert (\chor (\endpoint p1; p1.gameFinished() && p1.returner.mark == p1.myMark ==> turnInvariant(p1, p2))); - inhale false; } else { - inhale false; p2.createNewMove(); p2.doMove(); if (p2.gameFinished()) { @@ -86,10 +80,12 @@ choreography Main() { } p1.turn := !p1.turn; p2.turn := !p2.turn; - // TODO: Remove when lightweight encoding + // Assumption required for shortcoming in backend. Can be removed after implementing the lightweight encoding. assume (\chor (\endpoint p1; p1.gameFinished()) == (\endpoint p2; p2.gameFinished())); } - inhale false; assume (\chor (\endpoint p1; p1.gameFinished()) == (\endpoint p2; p2.gameFinished())); + + p1.finish(); + p2.finish(); } } diff --git a/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/Move.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Move.pvl similarity index 100% rename from examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/Move.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Move.pvl diff --git a/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/Player.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl similarity index 98% rename from examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/Player.pvl rename to examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl index 6dab65cee7..b7be576e8c 100644 --- a/examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/Player.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl @@ -190,6 +190,8 @@ class Player { ensures readMoveCell(move,this) == -1; void createNewMove(); + // Hook for the test suite to replace code + void finish() { } } requires Perm(move.i,read) ** Perm(move.j,read); diff --git a/examples/publications/2024/IFM2024VeyMontPermissions/reference.bib b/examples/publications/2024/IFM2024VeyMontPermissions/reference.bib new file mode 100644 index 0000000000..17512ba579 --- /dev/null +++ b/examples/publications/2024/IFM2024VeyMontPermissions/reference.bib @@ -0,0 +1,6 @@ +@inproceedings{Rubbens2024, + author = {Robert Rubbens and Petra van den Bos and Marieke Huisman}, + title = {VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory}, + publisher = {Springer}, + year = {2024} +} diff --git a/examples/publications/2024/IFM2024VeyMontPermissions/testFiles/patches.txt b/examples/publications/2024/IFM2024VeyMontPermissions/testFiles/patches.txt new file mode 100644 index 0000000000..e64c2570f9 --- /dev/null +++ b/examples/publications/2024/IFM2024VeyMontPermissions/testFiles/patches.txt @@ -0,0 +1,50 @@ +Give createNewMove a concrete implementation: +<<<<<<< + void createNewMove() { throw new UnsupportedOperationException(); } +======= + // Picks the first free move + void createNewMove() { + if (this.c00 == -1) { + this.move = new Move(0, 0, myMark); + } else if (this.c01 == -1) { + this.move = new Move(0, 1, myMark); + } else if (this.c02 == -1) { + this.move = new Move(0, 2, myMark); + } else if (this.c10 == -1) { + this.move = new Move(1, 0, myMark); + } else if (this.c11 == -1) { + this.move = new Move(1, 1, myMark); + } else if (this.c12 == -1) { + this.move = new Move(1, 2, myMark); + } else if (this.c20 == -1) { + this.move = new Move(2, 0, myMark); + } else if (this.c21 == -1) { + this.move = new Move(2, 1, myMark); + } else if (this.c22 == -1) { + this.move = new Move(2, 2, myMark); + } + } +>>>>>>> + +Save the final board of p1: +<<<<<<< +this.p1.impl.finish(); +======= +G$.p1Impl = this.p1.impl; +>>>>>>> + +Save the final board of p1: +<<<<<<< +this.p2.impl.finish(); +======= +G$.p2Impl = this.p2.impl; +>>>>>>> + +Add global fields to G$: +<<<<<<< +class G$ extends Thread { +======= +class G$ extends Thread { + public static Player p1Impl = null; + public static Player p2Impl = null; +>>>>>>> \ No newline at end of file diff --git a/examples/publications/2024/IFM2024VeyMontPermissions/testFiles/testScript.txt b/examples/publications/2024/IFM2024VeyMontPermissions/testFiles/testScript.txt new file mode 100644 index 0000000000..3331412126 --- /dev/null +++ b/examples/publications/2024/IFM2024VeyMontPermissions/testFiles/testScript.txt @@ -0,0 +1,31 @@ +new G$().main(); + +System.out.println( + "p1:\n" + + G$.p1Impl.c00 + " " + + G$.p1Impl.c01 + " " + + G$.p1Impl.c02 + "\n" + + + G$.p1Impl.c10 + " " + + G$.p1Impl.c11 + " " + + G$.p1Impl.c12 + "\n" + + + G$.p1Impl.c20 + " " + + G$.p1Impl.c21 + " " + + G$.p1Impl.c22 +); + +System.out.println( + "p2:\n" + + G$.p2Impl.c00 + " " + + G$.p2Impl.c01 + " " + + G$.p2Impl.c02 + "\n" + + + G$.p2Impl.c10 + " " + + G$.p2Impl.c11 + " " + + G$.p2Impl.c12 + "\n" + + + G$.p2Impl.c20 + " " + + G$.p2Impl.c21 + " " + + G$.p2Impl.c22 +); diff --git a/examples/technical/veymont/first.pvl b/examples/technical/veymont/first.pvl index 2d3f6707b7..1c48b2072f 100644 --- a/examples/technical/veymont/first.pvl +++ b/examples/technical/veymont/first.pvl @@ -16,7 +16,7 @@ choreography Example() { ensures Perm[alice](alice.x, 1) ** (\[alice] alice.x == 4); run { bob: alice.x := alice.x + 1; - channel_invariant Perm(alice.x, 1) ** alice.x == 3; + channel_invariant Perm(\receiver.x, 1) ** \receiver.x == 3; communicate bob.temp -> alice.temp; alice.x := alice.x + 1; } diff --git a/res/universal/res/veymont/genericChannel.pvl b/res/universal/res/veymont/genericChannel.pvl index 6a074d935e..0626c6e7a8 100644 --- a/res/universal/res/veymont/genericChannel.pvl +++ b/res/universal/res/veymont/genericChannel.pvl @@ -15,13 +15,13 @@ class Channel { loop_invariant Perm(hasMsg, 1) ** Perm(exchangeValue,1); loop_invariant held(this); - while (!hasMsg) { - unlock this; - lock this; + while (hasMsg) { + wait this; } - hasMsg = false; + hasMsg = true; exchangeValue = v; + notify this; unlock this; } @@ -31,12 +31,13 @@ class Channel { loop_invariant Perm(hasMsg, 1) ** Perm(exchangeValue,1); loop_invariant held(this); - while (hasMsg) { + while (!hasMsg) { wait this; } T m = exchangeValue; hasMsg = false; + notify this; unlock this; return m; diff --git a/src/col/vct/col/ast/declaration/cls/InstanceFunctionImpl.scala b/src/col/vct/col/ast/declaration/cls/InstanceFunctionImpl.scala index 049cd380ad..908735d4f6 100644 --- a/src/col/vct/col/ast/declaration/cls/InstanceFunctionImpl.scala +++ b/src/col/vct/col/ast/declaration/cls/InstanceFunctionImpl.scala @@ -12,12 +12,29 @@ trait InstanceFunctionImpl[G] extends InstanceFunctionOps[G] { ListMap(inline -> "inline", threadLocal -> "thread_local").filter(_._1) .values.map(Text).map(Doc.inlineSpec).toSeq - override def layout(implicit ctx: Ctx): Doc = + def layoutJava(implicit ctx: Ctx): Doc = + Doc.stack(Seq( + contract, + Group( + Doc.rspread(layoutModifiers) <> Doc.inlineSpec(Text("pure")) <+> + returnType <+> ctx.name(this) <> + (if (typeArgs.nonEmpty) + Text("<") <> Doc.args(typeArgs.map(ctx.name).map(Text)) <> ">" + else + Empty) <> "(" <> Doc.args(args) <> ")" <> body.map(body => + Text(" ") <> "{" <>> + // TODO (RR, PB): Why must the "return body" part be parenthesized here? + (Text("return") <+> Nest(body.show)) <> ";" <+/> "}" + ).getOrElse(Text(";")) + ), + )) + + def layoutPvl(implicit ctx: Ctx): Doc = Doc.stack(Seq( contract, Group( - Doc.rspread(layoutModifiers) <> Text("pure") <+> returnType <+> - ctx.name(this) <> + Doc.rspread(layoutModifiers) <> Doc.inlineSpec(Text("pure")) <+> + returnType <+> ctx.name(this) <> (if (typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs.map(ctx.name).map(Text)) <> ">" else @@ -25,4 +42,10 @@ trait InstanceFunctionImpl[G] extends InstanceFunctionOps[G] { body.map(Text(" =") <>> _ <> ";").getOrElse(Text(";")) ), )) + + override def layout(implicit ctx: Ctx): Doc = + ctx.syntax match { + case Ctx.Java => layoutJava + case Ctx.PVL => layoutPvl + } } diff --git a/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala b/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala index 378d7d7600..8aeed9bbc2 100644 --- a/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala +++ b/src/col/vct/col/ast/declaration/cls/InstanceMethodImpl.scala @@ -39,7 +39,7 @@ trait InstanceMethodImpl[G] Empty) } - override def layout(implicit ctx: Ctx): Doc = + def layoutPvl(implicit ctx: Ctx): Doc = Doc.stack(Seq( contract, Group( @@ -53,6 +53,27 @@ trait InstanceMethodImpl[G] Empty) <> body.map(Text(" ") <> _.layoutAsBlock).getOrElse(Text(";")), )) + def layoutJava(implicit ctx: Ctx): Doc = + Doc.stack(Seq( + contract, + Group( + Group( + Doc.rspread(layoutModifiers) <> returnType <+> layoutNameAndArgs + ) <> "(" <> Doc.args(args) <> ")" + ) <> + (if (outArgs.nonEmpty) + Text(" returns") <+> "(" <> Doc.args(outArgs) <> ")" + else + Empty) <> body.map(Text(" ") <> _.layoutAsBlock) + .getOrElse(Text(" { throw new UnsupportedOperationException(); }")), + )) + + override def layout(implicit ctx: Ctx): Doc = + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => layoutPvl + } + override def check(context: CheckContext[G]): Seq[CheckError] = context.currentChoreography match { case None => Seq() diff --git a/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala b/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala index 61d407826f..78ce6ede7d 100644 --- a/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala +++ b/src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala @@ -16,10 +16,13 @@ trait InstancePredicateImpl[G] ListMap(inline -> "inline", threadLocal -> "thread_local").filter(_._1) .values.map(Text).map(Doc.inlineSpec).toSeq - override def layout(implicit ctx: Ctx): Doc = - Group( + override def layout(implicit ctx: Ctx): Doc = { + val oldCtx = ctx + Group(Doc.spec { + implicit val ctx = oldCtx.copy(inSpec = oldCtx.syntax == Ctx.Java) Doc.rspread(layoutModifiers) <> "resource" <+> ctx.name(this) <> "(" <> Doc.args(args) <> ")" <> body.map(Text(" =") <>> _ <> ";") .getOrElse(Text(";")) - ) + }) + } } diff --git a/src/col/vct/col/ast/declaration/cls/RunMethodImpl.scala b/src/col/vct/col/ast/declaration/cls/RunMethodImpl.scala index 1171331f45..2c3d1d1db6 100644 --- a/src/col/vct/col/ast/declaration/cls/RunMethodImpl.scala +++ b/src/col/vct/col/ast/declaration/cls/RunMethodImpl.scala @@ -1,14 +1,28 @@ package vct.col.ast.declaration.cls -import vct.col.ast.RunMethod +import vct.col.ast.{RunMethod, TVoid} import vct.col.print._ import vct.col.ast.ops.RunMethodOps trait RunMethodImpl[G] extends RunMethodOps[G] { this: RunMethod[G] => - override def layout(implicit ctx: Ctx): Doc = + + def layoutJava(implicit ctx: Ctx): Doc = + Doc.stack(Seq( + contract.show, + Text("public") <+> TVoid().show <+> "run" <> "()" <+> + body.map(_.layoutAsBlock).getOrElse(Text("{ /*@ assume false; @*/ }")), + )) + + def layoutPvl(implicit ctx: Ctx): Doc = Doc.stack(Seq( contract.show, Text("run") <> body.map(Empty <+> _.layoutAsBlock).getOrElse(Text(";")), )) + + override def layout(implicit ctx: Ctx): Doc = + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => layoutPvl + } } diff --git a/src/col/vct/col/ast/declaration/global/ClassImpl.scala b/src/col/vct/col/ast/declaration/global/ClassImpl.scala index e28762c8e5..251557ee8d 100644 --- a/src/col/vct/col/ast/declaration/global/ClassImpl.scala +++ b/src/col/vct/col/ast/declaration/global/ClassImpl.scala @@ -50,13 +50,38 @@ trait ClassImpl[G] extends Declarator[G] { override def declarations: Seq[Declaration[G]] = decls ++ typeArgs def layoutLockInvariant(implicit ctx: Ctx): Doc = - Text("lock_invariant") <+> intrinsicLockInvariant <> ";" <+/> Empty + Text("lock_invariant") <+> Nest(intrinsicLockInvariant.show) <> ";" <+/> + Empty - override def layout(implicit ctx: Ctx): Doc = + def layoutLock(implicit ctx: Ctx): Doc = + Text("Lock") <+> "intrinsicLock$" <+> "=" <+> "new" <+> + "ReentrantLock(true);" <+/> "Condition" <+> "condition$" <+> "=" <+> + "intrinsicLock$" <> "." <> "newCondition()" <> ";" + + def layoutJava(implicit ctx: Ctx): Doc = (if (intrinsicLockInvariant == tt[G]) Empty else - Doc.spec(Show.lazily(layoutLockInvariant(_)))) <> Group( + Doc.spec(Show.lazily(layoutLockInvariant(_)))) <+/> Group( + Text("class") <+> ctx.name(this) <> + (if (typeArgs.nonEmpty) + Text("<") <> Doc.args(typeArgs) <> ">" + else + Empty) <> + (if (supports.isEmpty) + // Inheritance still needs work anyway + Text(" ") <> "extends" <+> "Thread" + else + Text(" ") <> "extends" <+> Doc.args( + supports.map(supp => ctx.name(supp.asClass.get.cls)).map(Text) + )) <+> "{" + ) <>> Doc.stack2(layoutLock +: decls) <+/> "}" + + def layoutPvl(implicit ctx: Ctx): Doc = + (if (intrinsicLockInvariant == tt[G]) + Empty + else + Doc.spec(Show.lazily(layoutLockInvariant(_)))) <+/> Group( Text("class") <+> ctx.name(this) <> (if (typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs) <> ">" @@ -68,5 +93,11 @@ trait ClassImpl[G] extends Declarator[G] { Text(" implements") <+> Doc.args( supports.map(supp => ctx.name(supp.asClass.get.cls)).map(Text) )) <+> "{" - ) <>> Doc.stack(decls) <+/> "}" + ) <>> Doc.stack2(decls) <+/> "}" + + override def layout(implicit ctx: Ctx): Doc = + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => layoutPvl + } } diff --git a/src/col/vct/col/ast/declaration/global/PredicateImpl.scala b/src/col/vct/col/ast/declaration/global/PredicateImpl.scala index f104760c31..66fc22dc57 100644 --- a/src/col/vct/col/ast/declaration/global/PredicateImpl.scala +++ b/src/col/vct/col/ast/declaration/global/PredicateImpl.scala @@ -24,11 +24,11 @@ trait PredicateImpl[G] .values.map(Text).map(Doc.inlineSpec).toSeq def layoutSpec(implicit ctx: Ctx): Doc = - Group( + Group(Doc.spec( Doc.rspread(layoutModifiers) <> "resource" <+> ctx.name(this) <> "(" <> Doc.args(args) <> ")" <> body.map(Text(" =") <>> _.show) - .getOrElse(Empty) - ) + .getOrElse(Empty) <> ";" + )) override def layout(implicit ctx: Ctx): Doc = ctx.syntax match { diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala index e9d496b278..f008cc3407 100644 --- a/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala +++ b/src/col/vct/col/ast/expr/heap/alloc/NewArrayImpl.scala @@ -3,6 +3,7 @@ package vct.col.ast.expr.heap.alloc import hre.util.FuncTools import vct.col.ast.{NewArray, TArray, Type} import vct.col.print._ +import vct.col.print.Doc.concat import vct.col.ast.ops.NewArrayOps trait NewArrayImpl[G] extends NewArrayOps[G] { @@ -12,6 +13,6 @@ trait NewArrayImpl[G] extends NewArrayOps[G] { override def precedence: Int = Precedence.POSTFIX override def layout(implicit ctx: Ctx): Doc = - Text("new") <+> element <> dims.map(dim => s"[$dim]").mkString <> + Text("new") <+> element <> concat(dims.map(Text("[") <> _ <> "]")) <> "[]".repeat(moreDims) } diff --git a/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala index 0a04b3f6ce..d9094cd3b7 100644 --- a/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceSupportsImpl.scala @@ -5,7 +5,7 @@ import vct.col.ast.ops.CoerceSupportsOps trait CoerceSupportsImpl[G] extends CoerceSupportsOps[G] { this: CoerceSupports[G] => - // TODO (RR): Integrate coercions with generics? + // TODO: Generics are not properly taken into account here override def target: TClass[G] = targetClass.decl.classType({ assert(sourceClass.decl.typeArgs.isEmpty); Seq() diff --git a/src/col/vct/col/ast/family/loopcontract/LoopInvariantImpl.scala b/src/col/vct/col/ast/family/loopcontract/LoopInvariantImpl.scala index f630b9d90e..1abc636d2c 100644 --- a/src/col/vct/col/ast/family/loopcontract/LoopInvariantImpl.scala +++ b/src/col/vct/col/ast/family/loopcontract/LoopInvariantImpl.scala @@ -6,8 +6,8 @@ import vct.col.ast.ops.LoopInvariantOps trait LoopInvariantImpl[G] extends LoopInvariantOps[G] { this: LoopInvariant[G] => - override def layout(implicit ctx: Ctx): Doc = - Doc.stack(Seq( + override def layout(implicit ctx: Ctx): Doc = { + Doc.spec(Doc.stack(Seq( Doc.stack(decreases.toSeq), DocUtil.clauses( if (ctx.syntax == Ctx.Silver) @@ -16,5 +16,6 @@ trait LoopInvariantImpl[G] extends LoopInvariantOps[G] { "loop_invariant", invariant, ), - )) + ))) + } } diff --git a/src/col/vct/col/ast/node/ProgramImpl.scala b/src/col/vct/col/ast/node/ProgramImpl.scala index bd482bfe59..c9cba63bc8 100644 --- a/src/col/vct/col/ast/node/ProgramImpl.scala +++ b/src/col/vct/col/ast/node/ProgramImpl.scala @@ -3,10 +3,10 @@ package vct.col.ast.node import vct.col.ast.{Node, Program} import vct.col.ast.util.Declarator import vct.col.check.{CheckContext, CheckError} -import vct.col.print.{Ctx, Doc} +import vct.col.print.{Ctx, Doc, Empty, Line, Text} import vct.col.util.CurrentCheckProgramContext import vct.result.VerificationError -import vct.col.ast.ops.{ProgramOps, ProgramFamilyOps} +import vct.col.ast.ops.{ProgramFamilyOps, ProgramOps} trait ProgramImpl[G] extends Declarator[G] with ProgramOps[G] with ProgramFamilyOps[G] { @@ -21,6 +21,12 @@ trait ProgramImpl[G] super.checkContextRecursor(context, f) } - override def layout(implicit ctx: Ctx): Doc = - Doc.fold(declarations)(_ <> vct.col.print.Line <> vct.col.print.Line <> _) + override def layout(implicit ctx: Ctx): Doc = { + (if (ctx.syntax == Ctx.Java) + (Text("import java.util.concurrent.locks.Lock;") <+/> + "import java.util.concurrent.locks.ReentrantLock;" <+/> + "import java.util.concurrent.locks.Condition;" <> Line) + else + Empty) <> Doc.stack2(declarations) + } } diff --git a/src/col/vct/col/ast/statement/exceptional/ReturnImpl.scala b/src/col/vct/col/ast/statement/exceptional/ReturnImpl.scala index c0a39fd96e..452e902a39 100644 --- a/src/col/vct/col/ast/statement/exceptional/ReturnImpl.scala +++ b/src/col/vct/col/ast/statement/exceptional/ReturnImpl.scala @@ -1,7 +1,7 @@ package vct.col.ast.statement.exceptional import vct.col.ast._ -import vct.col.print.{Ctx, Doc, Empty, Text} +import vct.col.print.{Ctx, Doc, Empty, Nest, Text} import vct.col.ast.ops.ReturnOps import vct.col.check.{CheckContext, CheckError, ReturnOutsideMethod} @@ -30,7 +30,7 @@ trait ReturnImpl[G] extends ExceptionalStatementImpl[G] with ReturnOps[G] { (if (result == Void[G]()) Text(";") else - Empty <+> result <> ";") + Empty <+> Nest(result.show) <> ";") override def expr: Expr[G] = this.result } diff --git a/src/col/vct/col/ast/statement/terminal/ForkImpl.scala b/src/col/vct/col/ast/statement/terminal/ForkImpl.scala index edb237ca80..f7389e9abb 100644 --- a/src/col/vct/col/ast/statement/terminal/ForkImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/ForkImpl.scala @@ -8,8 +8,14 @@ trait ForkImpl[G] extends ForkOps[G] { this: Fork[G] => def layoutSpec(implicit ctx: Ctx): Doc = Text("fork") <+> obj <> ";" + def layoutJava(implicit ctx: Ctx): Doc = obj.show <> ".start()" <> ";" + override def layout(implicit ctx: Ctx): Doc = - Doc.inlineSpec(Show.lazily(layoutSpec(_))) + ctx.syntax match { + case Ctx.Java => layoutJava + case Ctx.PVL => layoutSpec + case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_))) + } override def expr: Expr[G] = this.obj } diff --git a/src/col/vct/col/ast/statement/terminal/JoinImpl.scala b/src/col/vct/col/ast/statement/terminal/JoinImpl.scala index 1d77797aa6..5676ac340c 100644 --- a/src/col/vct/col/ast/statement/terminal/JoinImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/JoinImpl.scala @@ -1,15 +1,26 @@ package vct.col.ast.statement.terminal import vct.col.ast.{Expr, Join} -import vct.col.print.{Ctx, Doc, Show, Text} +import vct.col.print.{Ctx, Doc, Group, Show, Text} import vct.col.ast.ops.JoinOps trait JoinImpl[G] extends JoinOps[G] { this: Join[G] => def layoutSpec(implicit ctx: Ctx): Doc = Text("join") <+> obj <> ";" + def layoutJava(implicit ctx: Ctx): Doc = + Group( + Text("try") <+> "{" <>> + (obj.show <> Text(".join()") <> ";") <+/> "}" <+> "catch" <+> "(" <> + "InterruptedException" <+> "e" <> ")" <+> "{" <+> "}" + ) + override def layout(implicit ctx: Ctx): Doc = - Doc.inlineSpec(Show.lazily(layoutSpec(_))) + ctx.syntax match { + case Ctx.Java => layoutJava + case Ctx.PVL => layoutSpec + case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_))) + } override def expr: Expr[G] = this.obj } diff --git a/src/col/vct/col/ast/statement/terminal/LockImpl.scala b/src/col/vct/col/ast/statement/terminal/LockImpl.scala index 4ada85438b..54a53e1ff0 100644 --- a/src/col/vct/col/ast/statement/terminal/LockImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/LockImpl.scala @@ -8,8 +8,13 @@ trait LockImpl[G] extends LockOps[G] { this: Lock[G] => def layoutSpec(implicit ctx: Ctx): Doc = Text("lock") <+> obj <> ";" + def layoutJava(implicit ctx: Ctx): Doc = obj.show <> ".intrinsicLock$.lock();" + override def layout(implicit ctx: Ctx): Doc = - Doc.inlineSpec(Show.lazily(layoutSpec(_))) + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_))) + } override def expr: Expr[G] = this.obj } diff --git a/src/col/vct/col/ast/statement/terminal/NotifyImpl.scala b/src/col/vct/col/ast/statement/terminal/NotifyImpl.scala index b362e81496..5720231a9d 100644 --- a/src/col/vct/col/ast/statement/terminal/NotifyImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/NotifyImpl.scala @@ -8,8 +8,15 @@ trait NotifyImpl[G] extends NotifyOps[G] { this: Notify[G] => def layoutSpec(implicit ctx: Ctx): Doc = Text("notify") <+> obj <> ";" + def layoutJava(implicit ctx: Ctx): Doc = + // Use signal/await as notify/wait does not work for extrinsic locks + obj.show <> ".condition$" <> ".signal()" <> ";" + override def layout(implicit ctx: Ctx): Doc = - Doc.inlineSpec(Show.lazily(layoutSpec(_))) + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_))) + } override def expr: Expr[G] = this.obj } diff --git a/src/col/vct/col/ast/statement/terminal/UnlockImpl.scala b/src/col/vct/col/ast/statement/terminal/UnlockImpl.scala index 455f2eb2e6..a84cbb3df0 100644 --- a/src/col/vct/col/ast/statement/terminal/UnlockImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/UnlockImpl.scala @@ -8,8 +8,14 @@ trait UnlockImpl[G] extends UnlockOps[G] { this: Unlock[G] => def layoutSpec(implicit ctx: Ctx): Doc = Text("unlock") <+> obj <> ";" + def layoutJava(implicit ctx: Ctx): Doc = + obj.show <> ".intrinsicLock$.unlock();" + override def layout(implicit ctx: Ctx): Doc = - Doc.inlineSpec(Show.lazily(layoutSpec(_))) + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_))) + } override def expr: Expr[G] = this.obj } diff --git a/src/col/vct/col/ast/statement/terminal/WaitImpl.scala b/src/col/vct/col/ast/statement/terminal/WaitImpl.scala index f97a7a588f..25f7948838 100644 --- a/src/col/vct/col/ast/statement/terminal/WaitImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/WaitImpl.scala @@ -8,8 +8,16 @@ trait WaitImpl[G] extends WaitOps[G] { this: Wait[G] => def layoutSpec(implicit ctx: Ctx): Doc = Text("wait") <+> obj <> ";" + def layoutJava(implicit ctx: Ctx): Doc = + // Use signal/await as notify/wait does not work for extrinsic locks + Text("try") <+> "{" <+> obj.show <> ".condition$" <> ".await();" <+> "}" <+> + "catch" <+> "(" <> "InterruptedException" <+> "e" <> ")" <+> "{" <+> "}" + override def layout(implicit ctx: Ctx): Doc = - Doc.inlineSpec(Show.lazily(layoutSpec(_))) + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_))) + } override def expr: Expr[G] = this.obj } diff --git a/src/col/vct/col/ast/statement/veymont/ChorStatementImpl.scala b/src/col/vct/col/ast/statement/veymont/ChorStatementImpl.scala index f396bc9518..42d657b548 100644 --- a/src/col/vct/col/ast/statement/veymont/ChorStatementImpl.scala +++ b/src/col/vct/col/ast/statement/veymont/ChorStatementImpl.scala @@ -12,8 +12,10 @@ import scala.collection.immutable.ListSet trait ChorStatementImpl[G] extends ChorStatementOps[G] with StatementImpl[G] { this: ChorStatement[G] => + + // use non-existent syntax to be explicit about presence of an internal node override def layout(implicit ctx: Ctx): Doc = - Text("/* choreographic statement */") <+/> inner + Text("\\\\chor_statement") <+/> inner def exprs: Seq[Expr[G]] = (inner match { diff --git a/src/col/vct/col/ast/statement/veymont/EndpointStatementImpl.scala b/src/col/vct/col/ast/statement/veymont/EndpointStatementImpl.scala index 4c115314f8..b59e983980 100644 --- a/src/col/vct/col/ast/statement/veymont/EndpointStatementImpl.scala +++ b/src/col/vct/col/ast/statement/veymont/EndpointStatementImpl.scala @@ -47,9 +47,10 @@ trait EndpointStatementImpl[G] override def layout(implicit ctx: Ctx): Doc = (endpoint match { - case Some(Ref(endpoint)) => Text(s"/* ${ctx.name(endpoint)}: */ ") - case None => Text("/* unlabeled endpoint statement */") <> Line - }) <> inner + case Some(Ref(endpoint)) => + Text(s"\\\\endpoint_statement") <+> ctx.name(endpoint) <> ";" + case None => Text("\\\\unlabeled_endpoint_statement") + }) <+> inner object eval { def enterCheckContextCurrentReceiverEndpoint( diff --git a/src/col/vct/col/ast/unsorted/ConstructorImpl.scala b/src/col/vct/col/ast/unsorted/ConstructorImpl.scala index cec2a2bdfc..b21395c865 100644 --- a/src/col/vct/col/ast/unsorted/ConstructorImpl.scala +++ b/src/col/vct/col/ast/unsorted/ConstructorImpl.scala @@ -10,7 +10,16 @@ trait ConstructorImpl[G] extends ConstructorOps[G] { override def returnType: TClass[G] = cls.decl.classType(cls.decl.typeArgs.map((v: Variable[G]) => TVar(v.ref))) - override def layout(implicit ctx: Ctx): Doc = { + def layoutJava(implicit ctx: Ctx): Doc = + Doc.stack(Seq( + contract, + Group( + Text(ctx.name(cls.decl)) <> DocUtil.javaGenericParams(typeArgs) <> + "(" <> Doc.args(args) <> ")" + ) <> body.map(Text(" ") <> _).getOrElse(Text(";")), + )) + + def layoutPvl(implicit ctx: Ctx): Doc = Doc.stack(Seq( contract, Group( @@ -18,5 +27,11 @@ trait ConstructorImpl[G] extends ConstructorOps[G] { Doc.args(args) <> ")" ) <> body.map(Text(" ") <> _).getOrElse(Text(";")), )) - } + + override def layout(implicit ctx: Ctx): Doc = + ctx.syntax match { + case Ctx.Java => layoutJava + case _ => layoutPvl + } + } diff --git a/src/col/vct/col/ast/unsorted/ConstructorInvocationImpl.scala b/src/col/vct/col/ast/unsorted/ConstructorInvocationImpl.scala index cd0b8d4f52..97e1e0376a 100644 --- a/src/col/vct/col/ast/unsorted/ConstructorInvocationImpl.scala +++ b/src/col/vct/col/ast/unsorted/ConstructorInvocationImpl.scala @@ -1,12 +1,14 @@ package vct.col.ast.unsorted +import vct.col.ast.expr.ExprImpl import vct.col.ast.{Class, ConstructorInvocation, TClass, Type, Variable} import vct.col.ast.ops.ConstructorInvocationOps import vct.col.print._ import scala.util.Try -trait ConstructorInvocationImpl[G] extends ConstructorInvocationOps[G] { +trait ConstructorInvocationImpl[G] + extends ConstructorInvocationOps[G] with ExprImpl[G] { this: ConstructorInvocation[G] => def cls: Class[G] = ref.decl.cls.decl @@ -24,4 +26,6 @@ trait ConstructorInvocationImpl[G] extends ConstructorInvocationOps[G] { DocUtil.givenYields(givenMap, yields), )) } + + override def precedence: Int = Precedence.ATOMIC } diff --git a/src/col/vct/col/print/Doc.scala b/src/col/vct/col/print/Doc.scala index 31310bdd4d..3d9c9e1280 100644 --- a/src/col/vct/col/print/Doc.scala +++ b/src/col/vct/col/print/Doc.scala @@ -30,6 +30,8 @@ case object Doc { def fold(docs: Iterable[Show])(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc = docs.map(_.show).filter(_.nonEmpty).reduceLeftOption(f).getOrElse(Empty) + def concat(docs: Iterable[Show])(implicit ctx: Ctx): Doc = fold(docs)(_ <> _) + def spread(docs: Iterable[Show])(implicit ctx: Ctx): Doc = fold(docs)(_ <+> _) def rspread(docs: Iterable[Show])(implicit ctx: Ctx): Doc = @@ -40,6 +42,9 @@ case object Doc { def stack(docs: Iterable[Show])(implicit ctx: Ctx): Doc = fold(docs)(_ <+/> _) + def stack2(docs: Iterable[Show])(implicit ctx: Ctx): Doc = + fold(docs)(_ <> Line <> Line <> _) + def arg(doc: Show)(implicit ctx: Ctx): Doc = Nest(NonWsLine <> doc) <> NonWsLine diff --git a/src/col/vct/col/print/Namer.scala b/src/col/vct/col/print/Namer.scala index bb0b728144..55f281beef 100644 --- a/src/col/vct/col/print/Namer.scala +++ b/src/col/vct/col/print/Namer.scala @@ -123,6 +123,9 @@ case class Namer[G](syntax: Ctx.Syntax) { stack.having(node) { node.subnodes.foreach(name) } node match { + case _: Constructor[G] => + case _: RunMethod[G] => + case _: PVLChorRun[G] => case decl: GlobalDeclaration[G] => nameKeyed(nearest { case _: Program[G] => () }, decl) case decl: ClassDeclaration[G] => nameKeyed(nearestClass, decl) diff --git a/src/col/vct/col/util/AstBuildHelpers.scala b/src/col/vct/col/util/AstBuildHelpers.scala index 241b377dda..80475a5e54 100644 --- a/src/col/vct/col/util/AstBuildHelpers.scala +++ b/src/col/vct/col/util/AstBuildHelpers.scala @@ -675,6 +675,45 @@ object AstBuildHelpers { inline, )(blame) + def constructor[G]( + blame: Blame[CallableFailure], + contractBlame: Blame[NontrivialUnsatisfiable], + cls: Ref[G, Class[G]], + args: Seq[Variable[G]] = Nil, + outArgs: Seq[Variable[G]] = Nil, + typeArgs: Seq[Variable[G]] = Nil, + body: Option[Statement[G]] = None, + requires: AccountedPredicate[G] = + UnitAccountedPredicate(tt[G])(constOrigin(true)), + ensures: AccountedPredicate[G] = + UnitAccountedPredicate(tt[G])(constOrigin(true)), + contextEverywhere: Expr[G] = tt[G], + signals: Seq[SignalsClause[G]] = Nil, + givenArgs: Seq[Variable[G]] = Nil, + yieldsArgs: Seq[Variable[G]] = Nil, + decreases: Option[DecreasesClause[G]] = Some( + DecreasesClauseNoRecursion[G]()(constOrigin("decreases")) + ), + inline: Boolean = false, + )(implicit o: Origin): Constructor[G] = + new Constructor( + cls, + args, + outArgs, + typeArgs, + body, + ApplicableContract( + requires, + ensures, + contextEverywhere, + signals, + givenArgs, + yieldsArgs, + decreases, + )(contractBlame), + inline, + )(blame) + def functionInvocation[G]( blame: Blame[InvocationFailure], ref: Ref[G, Function[G]], diff --git a/src/hre/hre/stages/Stages.scala b/src/hre/hre/stages/Stages.scala index 97380ef3b8..a54bdbc75d 100644 --- a/src/hre/hre/stages/Stages.scala +++ b/src/hre/hre/stages/Stages.scala @@ -1,6 +1,8 @@ package hre.stages +import com.typesafe.scalalogging.LazyLogging import hre.progress.Progress +import hre.util.Time import vct.result.VerificationError trait Stage[-Input, +Output] { @@ -28,6 +30,10 @@ trait Stage[-Input, +Output] { UnitStages(this).thenRun(FunctionStage[Output, Output](x => { f; x })) } + def drop(): Stages[Input, Unit] = { + UnitStages(this).thenRun(FunctionStage[Output, Unit](_ => {})) + } + def preprocess[Input2](f: Input2 => Input): Stages[Input2, Output] = UnitStages(FunctionStage(f)).thenRun(UnitStages(this)) } @@ -60,8 +66,13 @@ object Stages { def skipIf[Input]( condition: Boolean, - stages: Stages[Input, Unit], - ): Stages[Input, Unit] = SkipIf(condition, stages) + stages: Stages[Input, Input], + ): Stages[Input, Input] = ApplyIf(!condition, stages) + + def applyIf[Input]( + condition: Boolean, + stages: Stages[Input, Input], + ): Stages[Input, Input] = ApplyIf(condition, stages) def branch[Input, Output]( condition: Boolean, @@ -73,6 +84,11 @@ object Stages { f: Input2 => Input, stages: Stages[Input, Output], ): Stages[Input2, Output] = UnitStages(FunctionStage(f)).thenRun(stages) + + def timed[Input, Output]( + name: String, + stages: Stages[Input, Output], + ): TimedStages[Input, Output] = TimedStages(name, stages) } trait Stages[-Input, +Output] { @@ -110,6 +126,9 @@ trait Stages[-Input, +Output] { def also(f: => Unit): Stages[Input, Output] = thenRun(FunctionStage[Output, Output](x => { val y = f; x })) + + def drop(): Stages[Input, Unit] = + thenRun(FunctionStage[Output, Unit](_ => {})) } case class FunctionStage[T, S](f: T => S) extends Stage[T, S] { @@ -163,13 +182,13 @@ case class SaveInputStage[Input, Output](stages: Stages[Input, Output]) } } -case class SkipIf[Input](condition: Boolean, stages: Stages[Input, Unit]) - extends Stages[Input, Unit] { +case class ApplyIf[Input](condition: Boolean, stages: Stages[Input, Input]) + extends Stages[Input, Input] { override def collect: Seq[Stage[Nothing, Any]] = if (condition) - Seq(FunctionStage((_: Input) => ())) - else stages.collect + else + Seq(FunctionStage((i: Input) => i)) } case class Branch[Input, Output]( @@ -183,3 +202,21 @@ case class Branch[Input, Output]( else ff.collect } + +case class TimedStages[Input, Output]( + name: String, + stages: Stages[Input, Output], +) extends Stages[Input, Output] with LazyLogging { + var start: java.time.Instant = null + var end: java.time.Instant = null + + override def collect: Seq[Stage[Nothing, Any]] = + IdentityStage().also { + start = java.time.Instant.now(); + logger.warn(s"Start: $name (at ${Time.formatTime(start)})") + }.collect ++ stages.collect ++ IdentityStage().also { + end = java.time.Instant.now(); + logger.warn(s"Done: $name (at ${Time.formatTime(end)}, duration: ${Time + .formatDuration(java.time.Duration.between(start, end))})") + }.collect +} diff --git a/src/hre/hre/util/FilesHelper.scala b/src/hre/hre/util/FilesHelper.scala new file mode 100644 index 0000000000..771033c65a --- /dev/null +++ b/src/hre/hre/util/FilesHelper.scala @@ -0,0 +1,45 @@ +package hre.util + +import java.io.IOException +import java.nio.file +import java.nio.file.attribute.BasicFileAttributes +import java.nio.file.{FileVisitResult, Files, Path, SimpleFileVisitor} + +case object FilesHelper { + def withTempDir[T](f: Path => T): T = { + val p = Files.createTempDirectory("java-veymont") + try { f(p) } + finally { deleteDirectory(p) } + } + + def deleteDirectory(p: Path) = { + require(file.Files.isDirectory(p)) + // Copied from the java standard library documentation + Files.walkFileTree( + p, + new SimpleFileVisitor[Path]() { + @throws[IOException] + override def visitFile( + file: Path, + attrs: BasicFileAttributes, + ): FileVisitResult = { + Files.delete(file) + FileVisitResult.CONTINUE + } + + @throws[IOException] + override def postVisitDirectory( + dir: Path, + e: IOException, + ): FileVisitResult = + if (e == null) { + Files.delete(dir) + FileVisitResult.CONTINUE + } else { + // directory iteration failed + throw e + } + }, + ) + } +} diff --git a/src/hre/hre/util/Patch.scala b/src/hre/hre/util/Patch.scala new file mode 100644 index 0000000000..e5c73569f3 --- /dev/null +++ b/src/hre/hre/util/Patch.scala @@ -0,0 +1,98 @@ +package hre.util + +import hre.util.Patch.{PatchException, UnappliablePatchException} + +import java.nio.file.{Files, Path, Paths} +import scala.annotation.tailrec +import scala.jdk.CollectionConverters._ +import scala.util.matching.Regex + +case object Patch { + class PatchException(msg: String) extends Exception(msg) + object NoPatchException extends PatchException("no patch found") + object UnappliablePatchException + extends PatchException("could not apply patch") + + def fromFile(p: Path): Seq[Patch] = parsePatches(Files.readString(p)) + + def parsePatches(str: String): Seq[Patch] = { + val (patch, rest) = parseFirstPatch(str) + if (rest.trim.isEmpty) + Seq(patch) + else + patch +: parsePatches(rest) + } + + // At least 7 characters per marker. Turn on DOTALL with (?s) to enable matching of newlines + val startMarker = "(?s)\n<<<<<<<+\n".r + val middleMarker = "(?s)\n=======+\n".r + val endMarker = "(?s)\n>>>>>>>+".r + + def parseFirstPatch(str: String): (Patch, String) = { + val start = startMarker.findFirstMatchIn(str) + .getOrElse(throw NoPatchException) + val startLength = start.end - start.start + assert(startLength >= 7 + 2) + + val middle = middleMarker.findFirstMatchIn(str) + .getOrElse(throw new PatchException("no middle marker")) + val end = endMarker.findFirstMatchIn(str) + .getOrElse(throw new PatchException("no end marker")) + val middleLength = middle.end - middle.start + val endLength = end.end - end.start + assert(middleLength >= 7 + 2 && endLength >= 7 + 1) + + // Subtract to accomodate for the newlines + if ( + startLength - 2 != middleLength - 2 || middleLength - 2 != endLength - 1 + ) + throw new PatchException( + s"length of start, middle and end markers do not match at ${start.start}" + ) + + ( + Patch( + str.substring(start.end, middle.start), + str.substring(middle.end, end.start), + ), + str.substring(end.end), + ) + } + + def main(args: Array[String]): Unit = { + if (args.length != 3) { + println( + "Incorrect number of arguments. Expected usage: `patcher [patch path] [input path] [output path]`" + ) + return + } + + val patchFile = Paths.get(args(0)) + val inFile = Paths.get(args(1)) + val outFile = Paths.get(args(2)) + + Files.writeString( + outFile, + applyAll(Patch.fromFile(patchFile), Files.readString(inFile)), + ) + + println( + s"Patched $inFile with patch in $patchFile and wrote result to $outFile" + ) + } + + def applyAll(patches: Seq[Patch], source: String): String = + patches.foldLeft(source) { case (source, patch) => patch.apply(source) } +} + +case class Patch(target: String, newText: String) { + lazy val r = Regex.quote(target).r + + final def apply(source: String): String = + r.findFirstMatchIn(source) match { + case Some(m) => + source.substring(0, m.start) + newText + + source.substring(m.end, source.length) + case None => throw UnappliablePatchException + } +} diff --git a/src/hre/hre/util/Time.scala b/src/hre/hre/util/Time.scala index 48dd4ed049..af5f3a4520 100644 --- a/src/hre/hre/util/Time.scala +++ b/src/hre/hre/util/Time.scala @@ -1,9 +1,11 @@ package hre.util +import com.typesafe.scalalogging.LazyLogging + import java.time.{Duration, Instant, LocalDateTime, ZoneId} import java.time.format.DateTimeFormatter -object Time { +object Time extends LazyLogging { def formatDuration(duration: Duration): String = f"${duration.toHoursPart}%02d:${duration.toMinutesPart}%02d:${duration.toSecondsPart}%02d" @@ -14,4 +16,22 @@ object Time { .withZone(ZoneId.systemDefault()) formatter.format(when) } + + def logTime[T](name: String, f: => T): T = { + logger.info(s"Start: $name (at ${formatTime()})") + val start = java.time.Instant.now() + try { f } + finally { + val duration = Duration.between(start, java.time.Instant.now()) + logger.info( + s"Done: $name (at ${formatTime()}, duration: ${formatDuration(duration)})" + ) + } + } +} + +case class Timer() { + val start = java.time.Instant.now() + + def end: Duration = Duration.between(start, java.time.Instant.now()) } diff --git a/src/main/vct/main/Main.scala b/src/main/vct/main/Main.scala index bb79f08414..f878ab89f1 100644 --- a/src/main/vct/main/Main.scala +++ b/src/main/vct/main/Main.scala @@ -12,7 +12,7 @@ import org.slf4j.LoggerFactory import scopt.OParser import vct.col.ast.Node import vct.debug.CrashReport -import vct.main.modes.{CFG, VeSUV, Verify, VeyMont} +import vct.main.modes.{CFG, Compile, Patcher, VeSUV, Verify, VeyMont} import vct.main.stages.Transformation import vct.options.Options import vct.options.types.Mode @@ -103,10 +103,8 @@ case object Main extends LazyLogging { } def runMode(mode: Mode, options: Options): Int = - options.mode match { - case Mode.Verify => - logger.info(s"Starting verification at ${hre.util.Time.formatTime()}") - Verify.runOptions(options) + mode match { + case Mode.Verify => Verify.runOptions(options) case Mode.HelpVerifyPasses => logger.info("Available passes:") Transformation.ofOptions(options).passes.foreach { pass => @@ -121,5 +119,7 @@ case object Main extends LazyLogging { case Mode.CFG => logger.info("Starting control flow graph transformation") CFG.runOptions(options) + case Mode.Compile => Compile.runOptions(options) + case Mode.Patcher => Patcher.runOptions(options) } } diff --git a/src/main/vct/main/modes/Compile.scala b/src/main/vct/main/modes/Compile.scala new file mode 100644 index 0000000000..39a6d29109 --- /dev/null +++ b/src/main/vct/main/modes/Compile.scala @@ -0,0 +1,31 @@ +package vct.main.modes + +import com.typesafe.scalalogging.LazyLogging +import vct.col.origin.BlameCollector +import vct.col.print.Ctx +import vct.col.rewrite.bip.BIP +import vct.main.Main +import vct.main.stages.{Output, Parsing, Resolution, Transformation} +import vct.options.Options +import vct.parsers.transform.ConstantBlameProvider + +import java.nio.file.Paths + +case object Compile extends LazyLogging { + def runOptions(options: Options): Int = { + if (options.inputs.isEmpty) { + logger.warn("No inputs given, not compiling anything") + } + + val collector = BlameCollector() + val blameProvider = ConstantBlameProvider(collector) + Parsing.ofOptions(options, blameProvider) + .thenRun(Resolution.ofOptions(options, blameProvider)) + .thenRun(Transformation.pvlJavaCompatOfOptions(options)).thenRun(Output( + options.compileOutput.orElse(Some(Paths.get("a.java"))), + Ctx.Java, + false, + )).run(options.inputs) + Main.EXIT_CODE_SUCCESS + } +} diff --git a/src/main/vct/main/modes/Patcher.scala b/src/main/vct/main/modes/Patcher.scala new file mode 100644 index 0000000000..15ab8ec250 --- /dev/null +++ b/src/main/vct/main/modes/Patcher.scala @@ -0,0 +1,65 @@ +package vct.main.modes + +import com.typesafe.scalalogging.LazyLogging +import hre.progress.Progress +import hre.util.Patch +import hre.util.Patch.NoPatchException +import vct.main.Main.{EXIT_CODE_ERROR, EXIT_CODE_SUCCESS} +import vct.options.Options +import vct.options.types.PathOrStd + +import java.nio.file.{FileAlreadyExistsException, Files} + +case object Patcher extends LazyLogging { + def runOptions(options: Options): Int = { + // Stages are not really necessary here, however without it Patcher might crash at the end because of a bug in Process.scala. + // When this is fixed the stages can be safely removed. + Progress.stages(Seq(("patching", 1))) { next => + val patches = + try { Patch.fromFile(options.patchFile) } + catch { + case NoPatchException => + logger.warn("Patch file is empty, not patching anything") + Seq() + } + + options.inputs match { + case Seq() => + logger.warn("No inputs given, not patching anything") + EXIT_CODE_SUCCESS + case Seq(in) => + logger.info(s"Applying patch `${options.patchFile}` to `${in.underlyingFile + .getOrElse("stdin")}`. Writing result to `${options.patchOutput}`") + Files.writeString( + options.patchOutput, + Patch.applyAll(patches, in.readToCompletion()), + ) + EXIT_CODE_SUCCESS + case inputs => + try { Files.createDirectories(options.patchOutput) } + catch { + case _: FileAlreadyExistsException => + logger.error("Output directory already exists as file") + return EXIT_CODE_ERROR + } + for (input <- inputs) { + val outputPath = + input match { + case PathOrStd.Path(path) => options.patchOutput.resolve(path) + case PathOrStd.StdInOrOut => + options.patchOutput.resolve("stdin") + } + logger.info( + s"Applying patch `${options.patchFile}` to `${input.underlyingFile + .getOrElse("stdin")}`. Writing result to `${outputPath}`" + ) + Files.writeString( + outputPath, + Patch.applyAll(patches, input.readToCompletion()), + ) + } + EXIT_CODE_SUCCESS + } + } + } +} diff --git a/src/main/vct/main/modes/Verify.scala b/src/main/vct/main/modes/Verify.scala index 974731d263..d0d6859fd2 100644 --- a/src/main/vct/main/modes/Verify.scala +++ b/src/main/vct/main/modes/Verify.scala @@ -4,6 +4,7 @@ import com.typesafe.scalalogging.LazyLogging import vct.options.Options import hre.io.{CollectString, Readable} import hre.util.Time +import hre.util.Time.logTime import sun.misc.{Signal, SignalHandler} import vct.col.origin.{BlameCollector, TableEntry, VerificationFailure} import vct.col.rewrite.bip.BIP @@ -93,9 +94,8 @@ case object Verify extends LazyLogging { case _: IllegalArgumentException => } - val start = java.time.Instant.now() - - try { + logTime( + "VerCors", verifyWithOptions(options, options.inputs) match { case Left(err: VerificationError.UserError) => logger.error(err.text) @@ -117,13 +117,8 @@ case object Verify extends LazyLogging { } friendlyHandleBipReport(report, options.bipReportFile) EXIT_CODE_VERIFICATION_FAILURE - } - } finally { - logger.info( - s"Finished verification at ${Time.formatTime()} (duration: ${Time - .formatDuration(Duration.between(start, java.time.Instant.now()))})" - ) - } + }, + ) } def friendlyHandleBipReport( diff --git a/src/main/vct/main/modes/VeyMont.scala b/src/main/vct/main/modes/VeyMont.scala index be1007d178..ca77c7490b 100644 --- a/src/main/vct/main/modes/VeyMont.scala +++ b/src/main/vct/main/modes/VeyMont.scala @@ -1,59 +1,260 @@ package vct.main.modes import com.typesafe.scalalogging.LazyLogging -import hre.io.CollectString -import hre.stages.Stage -import vct.col.origin.{BlameCollector, VerificationFailure} -import vct.main.Main.{EXIT_CODE_ERROR, EXIT_CODE_SUCCESS} -import vct.main.stages.Stages +import hre.io.{CollectString, LiteralReadable, Readable} +import hre.progress.Progress +import hre.stages.{IdentityStage, Stage, Stages} +import hre.stages.Stages.{applyIf, branch, saveInput, timed} +import hre.util.Time.logTime +import hre.util.{Time, Timer} +import vct.col.ast.Verification +import vct.col.origin.{BlameCollector, TableEntry, VerificationFailure} +import vct.col.print.Ctx +import vct.col.rewrite.Generation +import vct.col.rewrite.bip.BIP +import vct.main.Main.{ + EXIT_CODE_ERROR, + EXIT_CODE_SUCCESS, + EXIT_CODE_VERIFICATION_FAILURE, +} +import vct.main.modes.Verify.logger +import vct.main.stages.{ + Backend, + ExpectedErrors, + Output, + Parsing, + Resolution, + Transformation, +} import vct.options.Options +import vct.parsers.transform.ConstantBlameProvider import vct.result.VerificationError -import vct.result.VerificationError.UserError +import vct.result.VerificationError.{SystemError, Unreachable, UserError} object VeyMont extends LazyLogging { - case class ChoreographyVerificationError(failures: Seq[VerificationFailure]) - extends UserError { - override def text: String = { - val fails = failures.map(_.desc).mkString("\n") - s"Verification of the input choreography failed because of the following failures:\n$fails" - } - - override def code: String = "veymont:choreographyVerificationFailed" + case object WrapVerificationError { + def wrap(codePrefix: String, textPrefix: String)( + error: VerificationError + ): VerificationError = + error match { + case error: UserError => WrapUserError(codePrefix, textPrefix, error) + case error: SystemError => WrapSystemError(textPrefix, error) + } + } + case class WrapUserError( + codePrefix: String, + textPrefix: String, + error: UserError, + ) extends UserError { + override def code: String = s"$codePrefix:${error.code}" + override def text: String = s"$textPrefix\n${error.text}" + } + case class WrapSystemError(textPrefix: String, error: SystemError) + extends SystemError { + override def text: String = s"$textPrefix\n${error.text}" } - case class ImplementationVerificationError(failures: Seq[VerificationFailure]) - extends UserError { - override def text: String = { - val fails = failures.map(_.desc).mkString("\n") - s"Verification of the generated implementation failed because of the following failuers:\n$fails" + def choreographyWithOptions( + options: Options, + inputs: Seq[Readable], + ): Either[VerificationError, ChoreographyResult] = { + Progress.stages(Seq(("Parsing", 2), ("Verification", 15))) { next => + val collector = BlameCollector() + val blameProvider = ConstantBlameProvider(collector) + val timer = Timer() + + val parsingStages = Parsing.ofOptions(options, blameProvider) + .thenRun(Resolution.ofOptions(options, blameProvider)) + + val wrap: VerificationError => VerificationError = WrapVerificationError + .wrap( + "choreography", + "The following error occurred during choreography verification:", + ) + + val program = + parsingStages.run(inputs) match { + case Left(err) => return Left(wrap(err)) + case Right(program) => program + } + + next() + + if (!options.veymontSkipChoreographyVerification) { + val verificationStages = Transformation + .ofOptions(options, BIP.VerificationResults()) + .thenRun(Backend.ofOptions(options)) + .thenRun(ExpectedErrors.ofOptions(options)) + + verificationStages.run(program) match { + case Left(error) => Left(wrap(error)) + case Right(()) => + val end = timer.end + logger.info( + s"Choreographic verification took: ${Time.formatDuration(end)}" + ) + Right(ChoreographyResult(program, collector.errs.toSeq)) + } + } else { + logger.warn("Skipping choreography verification") + Right(ChoreographyResult(program, Seq())) + } } + } - override def code: String = "veymont:implementationVerificationFailed" + def generateWithOptions( + options: Options, + program: Verification[_ <: Generation], + ): Either[VerificationError, GenerateResult] = { + val generateJava = options.veymontOutput + .exists(_.toString.endsWith(".java")) + val generateStages = Transformation + .veymontImplementationGenerationOfOptions(options) + .thenRun(applyIf[Verification[_ <: Generation]]( + generateJava, + IdentityStage().thenRun(Transformation.pvlJavaCompatOfOptions(options)), + )).thenRun(Output( + options.veymontOutput, + if (generateJava) + Ctx.Java + else + Ctx.PVL, + false, + )) + val wrap: VerificationError => VerificationError = + WrapVerificationError.wrap( + "generate", + "The following error occurred while generating an implementation:", + )(_) + generateStages.run(program) match { + case Left(err) => Left(wrap(err)) + case Right(Seq(lit)) => + logger.info("Implementation generated successfully") + Right(GenerateResult(lit)) + case Right(_) => + Left(wrap(Unreachable("Code generation should only return 1 readable"))) + } } - case class NoVerificationFailures( - collector: BlameCollector, - error: Seq[VerificationFailure] => UserError, - ) extends Stage[Unit, Unit] { - override def friendlyName: String = "noVerificationErrors" - override def progressWeight: Int = 1 - override def run(in: Unit): Unit = - if (collector.errs.nonEmpty) { throw error(collector.errs.toSeq) } + def implementationWithOptions( + options: Options, + implementation: LiteralReadable, + ): Either[VerificationError, ImplementationResult] = { + val collector = BlameCollector() + val bipResults = BIP.VerificationResults() + val blameProvider = ConstantBlameProvider(collector) + + val stages = vct.main.stages.Stages.ofOptions( + options.copy(generatePermissions = false), + blameProvider, + bipResults, + ) + + if (!options.veymontSkipImplementationVerification) { + val timer = Timer() + stages.run(Seq(implementation)) match { + case Left(err) => + Left( + WrapVerificationError.wrap( + "implementation", + "The following error occurred during verification of the implementation:", + )(err) + ) + case Right(()) => + val end = timer.end + logger.info( + s"Implementation verification took: ${Time.formatDuration(end)}" + ) + Right(ImplementationResult(collector.errs.toSeq)) + } + } else { + logger.warn("Skipping implementation verification") + Right(ImplementationResult(collector.errs.toSeq)) + } } - def runOptions(options: Options): Int = { - val stages = Stages.veymontOfOptions(options) - stages.run(options.inputs) match { - case Left(err: VerificationError.UserError) => - logger.error(err.text) - EXIT_CODE_ERROR - case Left(err: VerificationError.SystemError) => - logger.error(CollectString(s => err.printStackTrace(s))) - EXIT_CODE_ERROR - case Right(()) => - logger.info("VeyMont success") - EXIT_CODE_SUCCESS + sealed trait StageResult + case class ChoreographyResult( + program: Verification[_ <: Generation], + failures: Seq[VerificationFailure], + ) extends StageResult + case class GenerateResult(implementation: LiteralReadable) extends StageResult + case class ImplementationResult(failures: Seq[VerificationFailure]) + extends StageResult + + // VeyMont entry point for tooling. Does not do post-processing of results. inputs argument is separate such that + // clients can inject both paths and string literals (LiteralReadable) + def ofOptions( + options: Options, + inputs: Seq[Readable], + ): Either[VerificationError, StageResult] = { + Progress.stages(Seq(("VeyMont", 1))) { _ => + Progress.stages( + Seq(("Choreography", 10), ("Generate", 2), ("Implementation", 9)) + ) { next => + val program = + choreographyWithOptions(options, inputs) match { + case Left(err) => return Left(err) + case res @ Right(ChoreographyResult(_, failures)) + if failures.nonEmpty => + return res + case Right(ChoreographyResult(program, Seq())) => program + } + + next() + + val implementation = + generateWithOptions(options, program) + .fold[GenerateResult](err => return Left(err), lit => lit) + .implementation + + next() + + implementationWithOptions(options, implementation) + } } } + // Main VeyMont entry point for human users. Acquires inputs from options object. + def runOptions(options: Options): Int = + logTime( + "VeyMont", + ofOptions(options, options.inputs) match { + case Left(err: VerificationError.UserError) => + logger.error(err.text) + EXIT_CODE_ERROR + case Left(err: VerificationError.SystemError) => + logger.error(CollectString(s => err.printStackTrace(s))) + EXIT_CODE_ERROR + case Right(result) => + result match { + case ChoreographyResult(_, fails) if fails.nonEmpty => + logger.error("Verification of choreography failed") + if (options.more || fails.size <= 2) + fails.foreach(fail => logger.error(fail.desc)) + else { + logger.info( + "Printing verification results as a compressed table. Run with `--more` for verbose verification results." + ) + logger.error(TableEntry.render(fails.map(_.asTableEntry))) + } + EXIT_CODE_VERIFICATION_FAILURE + case ChoreographyResult(_, _) => EXIT_CODE_SUCCESS + case GenerateResult(_) => EXIT_CODE_SUCCESS + case ImplementationResult(fails) if fails.nonEmpty => + logger.error("Verification of generated implementation failed") + if (options.more || fails.size <= 2) + fails.foreach(fail => logger.error(fail.desc)) + else { + logger.info( + "Printing verification results as a compressed table. Run with `--more` for verbose verification results." + ) + logger.error(TableEntry.render(fails.map(_.asTableEntry))) + } + EXIT_CODE_VERIFICATION_FAILURE + case ImplementationResult(_) => EXIT_CODE_SUCCESS + } + }, + ) + } diff --git a/src/main/vct/main/stages/Output.scala b/src/main/vct/main/stages/Output.scala index bacd2ecce6..94aca8e9ef 100644 --- a/src/main/vct/main/stages/Output.scala +++ b/src/main/vct/main/stages/Output.scala @@ -19,11 +19,6 @@ import vct.parsers.ParseResult import java.nio.charset.StandardCharsets import java.nio.file.{Files, Path} -/* TODO (RR): I messed this up for VeyMont & VeSUV, need to coordinate with Philip to get it in a nice shape - Philip does use the splitting up feature, so I'd need to rework that either into Output or into a separate stage - Also the writing to file feature he relies on. - */ - case object Output { def vesuvOfOptions[G <: Generation]( options: Options @@ -38,15 +33,8 @@ case object Output { Some(options.vesuvOutput), Ctx.PVL, Files.isDirectory(options.vesuvOutput), - )).thenRun(FunctionStage((_: Seq[LiteralReadable]) => - () - )) // TODO: Not the prettiest, but I have no time for this. I blame Bob. + )).thenRun(FunctionStage((_: Seq[LiteralReadable]) => ())) } - - def veymontOfOptions( - options: Options - ): Stage[Verification[_ <: Generation], Seq[LiteralReadable]] = - Output(options.veymontOutput, Ctx.PVL, false) } case class Output(out: Option[Path], syntax: Ctx.Syntax, splitDecls: Boolean) diff --git a/src/main/vct/main/stages/Resolution.scala b/src/main/vct/main/stages/Resolution.scala index 64aa310b13..a377e56d80 100644 --- a/src/main/vct/main/stages/Resolution.scala +++ b/src/main/vct/main/stages/Resolution.scala @@ -67,7 +67,7 @@ case object Resolution { case ClassPathEntry.SourcePath(root) => ResolveTypes.JavaClassPathEntry.Path(root) }, - options.veymontGeneratePermissions, + options.generatePermissions, options.devVeymontAllowAssign, ) } @@ -117,7 +117,7 @@ case class Resolution[G <: Generation]( ResolveTypes.JavaClassPathEntry.Path(Resources.getJrePath), ResolveTypes.JavaClassPathEntry.SourcePackageRoot, ), - veymontGeneratePermissions: Boolean = false, + generatePermissions: Boolean = false, veymontAllowAssign: Boolean = false, ) extends Stage[ParseResult[G], Verification[_ <: Generation]] with LazyLogging { @@ -147,7 +147,7 @@ case class Resolution[G <: Generation]( case some => throw InputResolutionError(some) } val resolvedProgram = LangSpecificToCol( - veymontGeneratePermissions, + generatePermissions, veymontAllowAssign, ).dispatch(typedProgram) resolvedProgram.check match { diff --git a/src/main/vct/main/stages/Stages.scala b/src/main/vct/main/stages/Stages.scala index beba65e6b2..3ede38da08 100644 --- a/src/main/vct/main/stages/Stages.scala +++ b/src/main/vct/main/stages/Stages.scala @@ -8,7 +8,7 @@ import vct.parsers.transform.{BlameProvider, ConstantBlameProvider} import vct.result.VerificationError import hre.io.{LiteralReadable, Readable} import hre.stages.{IdentityStage, Stages} -import hre.stages.Stages.{branch, saveInput} +import hre.stages.Stages.{applyIf, branch, saveInput, timed} import vct.col.origin.{BlameCollector, VerificationFailure} import vct.col.rewrite.bip.BIP import vct.main.modes.VeyMont @@ -16,6 +16,7 @@ import vct.parsers.ParseResult import viper.api.backend.carbon.Carbon import viper.api.backend.silicon.Silicon import com.typesafe.scalalogging.LazyLogging +import vct.col.print.Ctx import scala.collection.mutable @@ -71,62 +72,6 @@ case object Stages extends LazyLogging { .thenRun(ExpectedErrors.ofOptions(options)) } - def veymontOfOptions(options: Options): Stages[Seq[Readable], Unit] = { - val choreographyStage - : Stages[Seq[Readable], Verification[_ <: Generation]] = { - val collector = BlameCollector() - val bipResults = BIP.VerificationResults() - val blameProvider = ConstantBlameProvider(collector) - - IdentityStage() - .also(logger.info("VeyMont choreography verifier & code generator")) - .thenRun(Parsing.ofOptions(options, blameProvider).also(logger.info( - "Finished parsing" - ))).thenRun(Resolution.ofOptions(options, blameProvider)) - .thenRun(saveInput[Verification[_ <: Generation], Any](branch( - !options.veymontSkipChoreographyVerification, - IdentityStage() - .also(logger.info("Verifying choreography with VerCors")) - .thenRun(Transformation.ofOptions(options, bipResults)) - .thenRun(Backend.ofOptions(options)) - .thenRun(ExpectedErrors.ofOptions(options)) - .thenRun(VeyMont.NoVerificationFailures( - collector, - VeyMont.ChoreographyVerificationError, - )), - IdentityStage() - .also(logger.warn("Skipping verifying choreography with VerCors")), - ))).transform(_._1) - } - - val generationStage - : Stages[Verification[_ <: Generation], Seq[LiteralReadable]] = { - IdentityStage().also(logger.info("Generating endpoint implementations")) - .thenRun(Transformation.veymontImplementationGenerationOfOptions( - options - )).thenRun(Output.veymontOfOptions(options)) - } - - val implementationVerificationStage = { - val collector = BlameCollector() - val bipResults = BIP.VerificationResults() - val blameProvider = ConstantBlameProvider(collector) - - Parsing.ofOptions(options, blameProvider) - .thenRun(Resolution.ofOptions(options, blameProvider)) - .thenRun(Transformation.ofOptions(options, bipResults)) - .thenRun(Backend.ofOptions(options)) - .thenRun(ExpectedErrors.ofOptions(options)) - .thenRun(VeyMont.NoVerificationFailures( - collector, - VeyMont.ImplementationVerificationError, - )) - } - - choreographyStage.thenRun(generationStage) - .thenRun(implementationVerificationStage) - } - def vesuvOfOptions( options: Options, blameProvider: BlameProvider, diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index ae99a9e155..22058a0f81 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -15,7 +15,6 @@ 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.StructureCheck import vct.importer.{PathAdtImporter, Util} import vct.main.Main.TemporarilyUnsupported import vct.main.stages.Transformation.{ @@ -40,9 +39,12 @@ import vct.rewrite.{ MonomorphizeClass, SmtlibToProverTypes, VariableToPointer, + GenerateSingleOwnerPermissions, } import vct.rewrite.lang.ReplaceSYCLTypes import vct.rewrite.veymont._ +import vct.rewrite.veymont.generation._ +import vct.rewrite.veymont.verification._ import java.nio.file.Path import java.nio.file.Files @@ -140,7 +142,7 @@ object Transformation extends LazyLogging { splitVerificationByProcedure = options.devSplitVerificationByProcedure, optimizeUnsafe = options.devUnsafeOptimization, - veymontGeneratePermissions = options.veymontGeneratePermissions, + generatePermissions = options.generatePermissions, veymontBranchUnanimity = options.veymontBranchUnanimity, ) } @@ -153,6 +155,7 @@ object Transformation extends LazyLogging { options.veymontResourcePath, options.getParserDebugOptions, ), + options.generatePermissions, onPassEvent = options.outputIntermediatePrograms .map(p => reportIntermediateProgram(p, "generate")).toSeq ++ @@ -160,6 +163,14 @@ object Transformation extends LazyLogging { writeOutFunctions(after, options.outputAfterPass), ) + def pvlJavaCompatOfOptions(options: Options): Transformation = + PvlJavaCompat(onPassEvent = + options.outputIntermediatePrograms + .map(p => reportIntermediateProgram(p, "pvlJavaCompat")).toSeq ++ + writeOutFunctions(before, options.outputBeforePass) ++ + writeOutFunctions(after, options.outputAfterPass) + ) + sealed trait TransformationEvent case object before extends TransformationEvent case object after extends TransformationEvent @@ -280,7 +291,7 @@ class Transformation( * Check that non-trivial contracts are satisfiable. * @param splitVerificationByProcedure * Splits verification into one task per procedure body. - * @param veymontGeneratePermissions + * @param generatePermissions * Generates permissions such that each callable requires full permissions * its arguments and any transitively reachable locations. * @param veymontBranchUnanimity @@ -302,7 +313,7 @@ case class SilverTransformation( checkSat: Boolean = true, splitVerificationByProcedure: Boolean = false, override val optimizeUnsafe: Boolean = false, - veymontGeneratePermissions: Boolean = false, + generatePermissions: Boolean = false, veymontBranchUnanimity: Boolean = true, ) extends Transformation( onPassEvent, @@ -355,16 +366,16 @@ case class SilverTransformation( // Also, VeyMont requires branches to be nested, instead of flat, because the false branch // may refine the set of participating endpoints BranchToIfElse, - GenerateChoreographyPermissions.withArg(veymontGeneratePermissions), + GenerateSingleOwnerPermissions.withArg(generatePermissions), InferEndpointContexts, - PushInChor.withArg(veymontGeneratePermissions), + PushInChor.withArg(generatePermissions), StratifyExpressions, StratifyUnpointedExpressions, DeduplicateChorGuards, EncodeChorBranchUnanimity.withArg(veymontBranchUnanimity), EncodeEndpointInequalities, EncodeChannels, - EncodePermissionStratification.withArg(veymontGeneratePermissions), + EncodePermissionStratification.withArg(generatePermissions), EncodeChoreography, // All VeyMont nodes should now be gone @@ -441,7 +452,6 @@ case class SilverTransformation( EncodeForPermWithValue, EncodeAutoValue, ExtractInlineQuantifierPatterns, - RewriteTriggerADTFunctions, MonomorphizeContractApplicables, // Silver compat (basically no new nodes) @@ -465,11 +475,13 @@ case class VeyMontImplementationGeneration( Resources.getVeymontPath, vct.parsers.debug.DebugOptions.NONE, ), + generatePermissions: Boolean, override val onPassEvent: Seq[PassEventHandler] = Nil, ) extends Transformation( onPassEvent, Seq( DropChorExpr, + GenerateSingleOwnerPermissions.withArg(generatePermissions), InferEndpointContexts, StratifyExpressions, StratifyUnpointedExpressions, @@ -480,3 +492,11 @@ case class VeyMontImplementationGeneration( PrettifyBlocks, ), ) + +// Compiles away several aspects of PVL that are not natively support in Java, which are too involved to handle +// ad-hoc in the pretty printer, or possibly for which the COL ast has no support yet +case class PvlJavaCompat(override val onPassEvent: Seq[PassEventHandler] = Nil) + extends Transformation( + onPassEvent, + Seq(ImplicationToTernary, EncodeGlobalApplicables), + ) diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala index 819a72ee1f..ce6236c485 100644 --- a/src/main/vct/options/Options.scala +++ b/src/main/vct/options/Options.scala @@ -300,22 +300,44 @@ case object Options { opt[Path]("path-c-preprocessor").valueName("") .action((path, c) => c.copy(cPreprocessorPath = path)) .text("Set the location of the C preprocessor binary"), + opt[Unit]("generate-permissions") + .action((_, c) => c.copy(generatePermissions = true)).text( + "Generates permissions for the entire program using a syntax-driven single-owner policy" + ), note(""), note("VeyMont Mode"), opt[Unit]("veymont").action((_, c) => c.copy(mode = Mode.VeyMont)).text( "Enable VeyMont mode: decompose the global program from the input files into several local programs that can be executed in parallel" ).children( + opt[Unit]("choreography").abbr("chor").action((_, c) => + c.copy(veymontSkipImplementationVerification = true) + ).text("Only perform verification of the choreography."), + opt[Unit]("implementation").abbr("impl") + .action((_, c) => c.copy(veymontSkipChoreographyVerification = true)) + .text("Only perform verification of the generated implementation."), + opt[Unit]("generate").abbr("gen").action((_, c) => + c.copy( + veymontSkipChoreographyVerification = true, + veymontSkipImplementationVerification = true, + ) + ).text( + "Only generate an implementation, and skip the choreography and implementation verification steps" + ), opt[Path]("veymont-output").valueName("") - .action((path, c) => c.copy(veymontOutput = Some(path))), + .action((path, c) => c.copy(veymontOutput = Some(path))).text( + "Indicates output path for generated implementation. The extension decides the output language: `.pvl` is PVL, `.java` is Java." + ), opt[Path]("veymont-resource-path").valueName("") .action((path, c) => c.copy(veymontResourcePath = path)), opt[Unit]("veymont-skip-choreography-verification") - .action((_, c) => c.copy(veymontSkipChoreographyVerification = true)), + .action((_, c) => c.copy(veymontSkipChoreographyVerification = true)) + .text( + "Do not verify choreographies, skipping to implementation generation & verification immediately" + ), + opt[Unit]("veymont-skip-implementation-verification").action((_, c) => + c.copy(veymontSkipImplementationVerification = true) + ).text("Do not verify generated implementation"), ), - 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" - ), opt[Unit]("dev-veymont-no-branch-unanimity").maybeHidden() .action((_, c) => c.copy(veymontBranchUnanimity = false)).text( "Disables generation of the branch unanimity check encoded by VeyMont, which verifies that choreographies do not deadlock during choreographic verification" @@ -361,6 +383,31 @@ case object Options { .text("Output file for the control flow graph in .dot format") ), note(""), + note("Compile mode"), + opt[Unit]("compile").action((_, c) => c.copy(mode = Mode.Compile)).text( + "Compiles PVL to Java. Currently only supported for the imperative fragment of PVL." + ).children( + opt[Path]("compile-output").valueName("") + .action((path, c) => c.copy(compileOutput = Some(path))) + .text("Output Java file") + ), + note(""), + note("Patcher mode"), + opt[Unit]("patcher").action((_, c) => c.copy(mode = Mode.Patcher)).text( + "Patches a file given a patch in the custom VerCors patch format." + ).children( + opt[Path]("patch-file").valueName("").required() + .action((path, c) => c.copy(patchFile = path)) + .text("Path to patch file to apply"), + opt[Path]("patch-output").valueName("").required().action( + (path, c) => c.copy(patchOutput = path) + ).text( + "Output path. If the patcher is given only one input, this is interpeted as a file destination." + + " " + + "If the patcher is given multiple inputs, this is interpreted as a directory path." + ), + ), + note(""), note(""), arg[PathOrStd]("...").unbounded().optional() .action((path, c) => c.copy(inputs = c.inputs :+ path)) @@ -428,6 +475,7 @@ case class Options( siliconPrintQuantifierStats: Option[Int] = None, bipReportFile: Option[PathOrStd] = None, inferHeapContextIntoFrame: Boolean = true, + generatePermissions: Boolean = false, // Verify options - hidden devParserReportAmbiguities: Boolean = false, @@ -456,9 +504,9 @@ case class Options( // VeyMont options veymontOutput: Option[Path] = None, veymontResourcePath: Path = Resources.getVeymontPath, - veymontGeneratePermissions: Boolean = false, veymontBranchUnanimity: Boolean = true, veymontSkipChoreographyVerification: Boolean = false, + veymontSkipImplementationVerification: Boolean = false, devVeymontAllowAssign: Boolean = false, // VeSUV options @@ -470,6 +518,13 @@ case class Options( // Control flow graph options cfgOutput: Path = null, + + // Compile options + compileOutput: Option[Path] = None, + + // Patch options + patchFile: Path = null, + patchOutput: Path = null, ) { def getParserDebugOptions: vct.parsers.debug.DebugOptions = vct.parsers.debug.DebugOptions( diff --git a/src/main/vct/options/types/Mode.scala b/src/main/vct/options/types/Mode.scala index 5405e70dc0..2c4c849c3c 100644 --- a/src/main/vct/options/types/Mode.scala +++ b/src/main/vct/options/types/Mode.scala @@ -9,4 +9,6 @@ case object Mode { case object VeyMont extends Mode case object VeSUV extends Mode case object CFG extends Mode + case object Compile extends Mode + case object Patcher extends Mode } diff --git a/src/parsers/antlr4/CPPParser.g4 b/src/parsers/antlr4/CPPParser.g4 index b7c20a2aac..26f736a6bd 100644 --- a/src/parsers/antlr4/CPPParser.g4 +++ b/src/parsers/antlr4/CPPParser.g4 @@ -1,7 +1,13 @@ parser grammar CPPParser; -options {tokenVocab = LangCPPLexer;} +options { + superClass = CPPParserBase; + tokenVocab = LangCPPLexer; +} import LangCPPParser, SpecParser; +@header { + import vct.parsers.parser.CPPParserBase; +} @parser::members { public int specLevel = 0; } diff --git a/src/parsers/antlr4/LangCPPParser.g4 b/src/parsers/antlr4/LangCPPParser.g4 index 25bfd184af..29fb6eca1c 100644 --- a/src/parsers/antlr4/LangCPPParser.g4 +++ b/src/parsers/antlr4/LangCPPParser.g4 @@ -427,27 +427,21 @@ typeSpecifierSeq: typeSpecifier+ attributeSpecifierSeq?; trailingTypeSpecifierSeq: trailingTypeSpecifier+ attributeSpecifierSeq?; -simpleTypeLengthModifier: - Short - | Long; - -simpleTypeSignednessModifier: - Unsigned - | Signed; - simpleTypeSpecifier: nestedNameSpecifier? theTypeName | nestedNameSpecifier Template simpleTemplateId - | simpleTypeSignednessModifier - | simpleTypeSignednessModifier? simpleTypeLengthModifier+ - | simpleTypeSignednessModifier? Char - | simpleTypeSignednessModifier? Char16 - | simpleTypeSignednessModifier? Char32 - | simpleTypeSignednessModifier? Wchar + | Char + | Char16 + | Char32 + | Wchar | Bool - | simpleTypeSignednessModifier? simpleTypeLengthModifier* Int + | Short + | Int + | Long + | Signed + | Unsigned | Float - | simpleTypeLengthModifier? Double + | Double | Void | Auto | {specLevel>0}? valType @@ -610,28 +604,22 @@ abstractDeclarator: | abstractPackDeclarator; pointerAbstractDeclarator: - noPointerAbstractDeclarator - | pointerOperatorWithDoubleStar+ noPointerAbstractDeclarator?; + pointerOperatorWithDoubleStar* (noPointerAbstractDeclarator | pointerOperatorWithDoubleStar); noPointerAbstractDeclarator: - noPointerAbstractDeclarator ( - parametersAndQualifiers - | noPointerAbstractDeclarator LeftBracket constantExpression? RightBracket - attributeSpecifierSeq? - ) - | parametersAndQualifiers - | LeftBracket constantExpression? RightBracket attributeSpecifierSeq? - | LeftParen pointerAbstractDeclarator RightParen; + (parametersAndQualifiers | LeftParen pointerAbstractDeclarator RightParen) ( + parametersAndQualifiers + | LeftBracket constantExpression? RightBracket attributeSpecifierSeq? + )*; abstractPackDeclarator: pointerOperatorWithDoubleStar* noPointerAbstractPackDeclarator; noPointerAbstractPackDeclarator: - noPointerAbstractPackDeclarator ( + Ellipsis ( parametersAndQualifiers | LeftBracket constantExpression? RightBracket attributeSpecifierSeq? - ) - | Ellipsis; + )*; parameterDeclarationClause: parameterDeclarationList parameterDeclarationVarargs?; @@ -713,11 +701,10 @@ memberDeclaratorList: memberDeclarator (Comma memberDeclarator)*; memberDeclarator: - declarator ( - virtualSpecifierSeq? pureSpecifier? - | braceOrEqualInitializer? - ) - | clangppIdentifier? attributeSpecifierSeq? Colon constantExpression; + declarator (virtualSpecifierSeq | { this.IsPureSpecifierAllowed() }? pureSpecifier | { this.IsPureSpecifierAllowed() }? virtualSpecifierSeq pureSpecifier | braceOrEqualInitializer) + | declarator + | clangppIdentifier? attributeSpecifierSeq? Colon constantExpression + ; virtualSpecifierSeq: virtualSpecifier+; @@ -727,8 +714,7 @@ virtualSpecifier: Override | Final; */ pureSpecifier: - Assign val = OctalLiteral {if($val.text.compareTo("0")!=0) throw new InputMismatchException(this); - }; + Assign IntegerLiteral; //Derived classes baseClause: Colon baseSpecifierList; diff --git a/src/parsers/vct/parsers/parser/CPPParserBase.java b/src/parsers/vct/parsers/parser/CPPParserBase.java new file mode 100644 index 0000000000..ae5bb48d2e --- /dev/null +++ b/src/parsers/vct/parsers/parser/CPPParserBase.java @@ -0,0 +1,28 @@ +package vct.parsers.parser; + +import org.antlr.v4.runtime.*; + +public abstract class CPPParserBase extends Parser +{ + protected CPPParserBase(TokenStream input) + { + super(input); + } + + protected boolean IsPureSpecifierAllowed() + { + try + { + var x = this._ctx; // memberDeclarator + var c = x.getChild(0).getChild(0); + var c2 = c.getChild(0); + var p = c2.getChild(1); + if (p == null) return false; + return (p instanceof vct.antlr4.generated.CPPParser.ParametersAndQualifiersContext); + } + catch (Exception e) + { + } + return false; + } +} \ No newline at end of file diff --git a/src/parsers/vct/parsers/transform/CPPToCol.scala b/src/parsers/vct/parsers/transform/CPPToCol.scala index 3a079b6606..4289339c58 100644 --- a/src/parsers/vct/parsers/transform/CPPToCol.scala +++ b/src/parsers/vct/parsers/transform/CPPToCol.scala @@ -897,53 +897,39 @@ case class CPPToCol[G]( case _ => ??(typeSpec) } case SimpleTypeSpecifier1(_, _, _) => ??(typeSpec) - case SimpleTypeSpecifier2(signedness) => Seq(convert(signedness)) - case SimpleTypeSpecifier3(Some(signedness), typeLengthMods) => - Seq(convert(signedness)) ++ typeLengthMods.map(convert(_)) - case SimpleTypeSpecifier3(None, typeLengthMods) => - typeLengthMods.map(convert(_)) - case SimpleTypeSpecifier4(Some(signedness), _) => - Seq(convert(signedness), new CPPChar[G]()) - case SimpleTypeSpecifier4(None, _) => Seq(new CPPChar[G]()) - case SimpleTypeSpecifier5(_, _) => ??(typeSpec) - case SimpleTypeSpecifier6(_, _) => ??(typeSpec) - case SimpleTypeSpecifier7(_, _) => ??(typeSpec) - case SimpleTypeSpecifier8(_) => Seq(new CPPBool[G]()) - case SimpleTypeSpecifier9(Some(signedness), typeLengthMods, _) => - Seq(convert(signedness)) ++ typeLengthMods.map(convert(_)) :+ - new CPPInt[G]() - case SimpleTypeSpecifier9(None, typeLengthMods, _) => - typeLengthMods.map(convert(_)) :+ new CPPInt[G]() - case SimpleTypeSpecifier10(_) => + // Char + case SimpleTypeSpecifier2(_) => Seq(new CPPChar[G]()) + // Char16 + case SimpleTypeSpecifier3(_) => ??(typeSpec) + // Char32 + case SimpleTypeSpecifier4(_) => ??(typeSpec) + // Wchar + case SimpleTypeSpecifier5(_) => ??(typeSpec) + // Bool + case SimpleTypeSpecifier6(_) => Seq(new CPPBool[G]()) + // Short + case SimpleTypeSpecifier7(_) => ??(typeSpec) + // Int + case SimpleTypeSpecifier8(_) => Seq(new CPPInt[G]()) + // Long + case SimpleTypeSpecifier9(_) => ??(typeSpec) + // Signed + case SimpleTypeSpecifier10(_) => Seq(new CPPSigned[G]()) + // Signed + case SimpleTypeSpecifier11(_) => Seq(new CPPUnsigned[G]()) + // Float + case SimpleTypeSpecifier12(_) => Seq(CPPSpecificationType(TFloats.C_ieee754_32bit)) - case SimpleTypeSpecifier11(Some(typeLengthMod), _) => - Seq( - convert(typeLengthMod), - CPPSpecificationType(TFloats.C_ieee754_64bit), - ) - case SimpleTypeSpecifier11(None, _) => + // Double + case SimpleTypeSpecifier13(_) => Seq(CPPSpecificationType(TFloats.C_ieee754_64bit)) - case SimpleTypeSpecifier12(_) => Seq(new CPPVoid[G]()) - case SimpleTypeSpecifier13(_) => ??(typeSpec) - case SimpleTypeSpecifier14(valType) => - Seq(CPPSpecificationType(convert(valType))) + // Void + case SimpleTypeSpecifier14(_) => Seq(new CPPVoid[G]()) + // Auto case SimpleTypeSpecifier15(_) => ??(typeSpec) - } - - def convert( - implicit signedness: SimpleTypeSignednessModifierContext - ): CPPTypeSpecifier[G] = - signedness match { - case SimpleTypeSignednessModifier0(_) => new CPPUnsigned[G]() - case SimpleTypeSignednessModifier1(_) => new CPPSigned[G]() - } - - def convert( - implicit simpleTypeLengthMod: SimpleTypeLengthModifierContext - ): CPPTypeSpecifier[G] = - simpleTypeLengthMod match { - case SimpleTypeLengthModifier0(_) => new CPPShort[G]() - case SimpleTypeLengthModifier1(_) => new CPPLong[G]() + case SimpleTypeSpecifier16(valType) => + Seq(CPPSpecificationType(convert(valType))) + case SimpleTypeSpecifier17(_) => ??(typeSpec) } // Do not support template or decltypes, or a typename as identifier in the nestedname diff --git a/src/rewrite/vct/rewrite/veymont/GenerateChoreographyPermissions.scala b/src/rewrite/vct/rewrite/GenerateSingleOwnerPermissions.scala similarity index 91% rename from src/rewrite/vct/rewrite/veymont/GenerateChoreographyPermissions.scala rename to src/rewrite/vct/rewrite/GenerateSingleOwnerPermissions.scala index fffac5ab9a..24ba02e8ff 100644 --- a/src/rewrite/vct/rewrite/veymont/GenerateChoreographyPermissions.scala +++ b/src/rewrite/vct/rewrite/GenerateSingleOwnerPermissions.scala @@ -1,24 +1,23 @@ -package vct.rewrite.veymont +package vct.rewrite import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack -import vct.col.util.AstBuildHelpers._ import vct.col.ast._ import vct.col.ast.declaration.global.ChoreographyImpl.participants import vct.col.origin.{Origin, PanicBlame} import vct.col.ref.Ref -import vct.col.resolve.ctx.Referrable import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg} +import vct.col.util.AstBuildHelpers._ -import scala.collection.immutable.ListSet +import scala.collection.mutable -object GenerateChoreographyPermissions extends RewriterBuilderArg[Boolean] { - override def key: String = "generateChoreographyPermissions" +object GenerateSingleOwnerPermissions extends RewriterBuilderArg[Boolean] { + override def key: String = "generateSingleOwnerPermissions" override def desc: String = "Generates permissions for fields of some types (classes, int, bool, and arrays of these) for constructs used inside choreographies." } -case class GenerateChoreographyPermissions[Pre <: Generation]( +case class GenerateSingleOwnerPermissions[Pre <: Generation]( enabled: Boolean = false ) extends Rewriter[Pre] with LazyLogging { @@ -83,7 +82,7 @@ case class GenerateChoreographyPermissions[Pre <: Generation]( ), ) - case cls: Class[Pre] if enabled => + case cls: ByReferenceClass[Pre] if enabled => currentPerm.having(classPerm(cls)) { cls.rewriteDefault().succeed(cls) } case fun: InstanceFunction[Pre] if enabled => @@ -239,7 +238,7 @@ case class GenerateChoreographyPermissions[Pre <: Generation]( def resultPerm(app: ContractApplicable[Pre])(implicit o: Origin): Expr[Post] = transitivePerm(Result[Post](anySucc(app)), app.returnType) - def classPerm(cls: Class[Pre]): Expr[Post] = + def classPerm(cls: ByReferenceClass[Pre]): Expr[Post] = transitivePerm(ThisObject[Post](succ(cls))(cls.o), cls.classType(Seq()))( cls.o ) @@ -260,6 +259,8 @@ case class GenerateChoreographyPermissions[Pre <: Generation]( */ + val warnedClasses = mutable.HashSet[Class[Pre]]() + def transitivePerm(e: Expr[Post], t: Type[Pre])( implicit o: Origin ): Expr[Post] = @@ -286,7 +287,8 @@ case class GenerateChoreographyPermissions[Pre <: Generation]( u, )), ) - case t: TClass[Pre] if !generatingClasses.contains(t.cls.decl) => + case t: TByReferenceClass[Pre] + if !generatingClasses.contains(t.cls.decl) => generatingClasses.having(t.cls.decl) { foldStar(t.cls.decl.collect { case f: InstanceField[Pre] => fieldTransitivePerm(e, f)(f.o) @@ -295,10 +297,13 @@ case class GenerateChoreographyPermissions[Pre <: Generation]( case t: TByReferenceClass[Pre] => // The class we are generating permission for has already been encountered when going through the chain // of fields. So we cut off the computation - logger.warn( - s"Not generating permissions for recursive occurrence of ${t.cls.decl - .o.getPreferredNameOrElse().ucamel}. Circular datastructures are not supported by permission generation" - ) + if (!warnedClasses.contains(t.cls.decl)) { + logger.warn( + s"Not generating permissions for recursive occurrence of ${t.cls + .decl.o.getPreferredNameOrElse().ucamel}. Circular datastructures are not supported by permission generation" + ) + warnedClasses.addOne(t.cls.decl) + } tt case _ => tt } @@ -308,7 +313,7 @@ case class GenerateChoreographyPermissions[Pre <: Generation]( ): Expr[Post] = { val left = fieldPerm[Post](`this`, succ(f), WritePerm()) f.t match { - case _: TClass[Pre] | _: TArray[Pre] => + case _: TByReferenceClass[Pre] | _: TArray[Pre] => left &* transitivePerm( Deref[Post](`this`, succ(f))(PanicBlame( "Permission for this field is already established" diff --git a/src/rewrite/vct/rewrite/RewriteTriggerADTFunctions.scala b/src/rewrite/vct/rewrite/RewriteTriggerADTFunctions.scala deleted file mode 100644 index 2cb6643009..0000000000 --- a/src/rewrite/vct/rewrite/RewriteTriggerADTFunctions.scala +++ /dev/null @@ -1,41 +0,0 @@ -package vct.col.rewrite - -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.util.AstBuildHelpers.VarBuildHelpers - -case object RewriteTriggerADTFunctions extends RewriterBuilder { - override def key: String = "rewriteTriggerADTFunctions" - override def desc: String = - "Rewrite adt forwarding functions in triggers to axiomatic ones." -} - -case class RewriteTriggerADTFunctions[Pre <: Generation]() - extends Rewriter[Pre] { - - val inTrigger: ScopedStack[Unit] = ScopedStack() - - override def dispatch(e: Expr[Pre]): Expr[Post] = - e match { - case f @ Forall(_, triggers, _) => - f.rewrite(triggers = - inTrigger.having(()) { triggers.map(_.map(dispatch)) } - ) - - case s @ Starall(_, triggers, _) => - s.rewrite(triggers = - inTrigger.having(()) { triggers.map(_.map(dispatch)) } - ) - - case e @ Exists(_, triggers, _) => - e.rewrite(triggers = - inTrigger.having(()) { triggers.map(_.map(dispatch)) } - ) - - case other => rewriteDefault(other) - - } -} diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala index 6db99e77dc..07f44d51a5 100644 --- a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala @@ -52,7 +52,7 @@ case object LangPVLToCol { case class LangPVLToCol[Pre <: Generation]( rw: LangSpecificToCol[Pre], - veymontGeneratePermissions: Boolean, + generatePermissions: Boolean, ) extends LazyLogging { type Post = Rewritten[Pre] implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw @@ -114,7 +114,7 @@ case class LangPVLToCol[Pre <: Generation]( AstBuildHelpers.foldStar(cls.decls.collect { case field: InstanceField[Pre] if field.flags.collectFirst { case _: Final[Pre] => () - }.isEmpty && !veymontGeneratePermissions => + }.isEmpty && !generatePermissions => fieldPerm[Post](`this`, rw.succ(field), WritePerm()) }) &* (if (checkRunnable) diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 2d4a8ed2d1..687c3adc07 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -33,14 +33,14 @@ case object LangSpecificToCol extends RewriterBuilderArg2[Boolean, Boolean] { } case class LangSpecificToCol[Pre <: Generation]( - veymontGeneratePermissions: Boolean = false, + generatePermissions: Boolean = false, veymontAllowAssign: 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, veymontGeneratePermissions) + val pvl: LangPVLToCol[Pre] = LangPVLToCol(this, generatePermissions) val veymont: LangVeyMontToCol[Pre] = LangVeyMontToCol( this, veymontAllowAssign, diff --git a/src/rewrite/vct/rewrite/veymont/ChannelInfo.scala b/src/rewrite/vct/rewrite/veymont/ChannelInfo.scala deleted file mode 100644 index c03d115b94..0000000000 --- a/src/rewrite/vct/rewrite/veymont/ChannelInfo.scala +++ /dev/null @@ -1,10 +0,0 @@ -package vct.rewrite.veymont - -import vct.col.ast.{Type, CommunicateX} -import vct.col.rewrite.Generation - -class ChannelInfo[Pre <: Generation]( - val comExpr: CommunicateX[Pre], - val channelType: Type[Pre], - val channelName: String, -) {} diff --git a/src/rewrite/vct/rewrite/veymont/DeduplicateChorGuards.scala b/src/rewrite/vct/rewrite/veymont/DeduplicateChorGuards.scala index 6915723606..6e3a54c718 100644 --- a/src/rewrite/vct/rewrite/veymont/DeduplicateChorGuards.scala +++ b/src/rewrite/vct/rewrite/veymont/DeduplicateChorGuards.scala @@ -15,6 +15,12 @@ object DeduplicateChorGuards extends RewriterBuilder { case class DeduplicateChorGuards[Pre <: Generation]() extends Rewriter[Pre] with VeymontContext[Pre] { + + override def dispatch(p: Program[Pre]): Program[Post] = { + mappings.program = p + super.dispatch(p) + } + override def dispatch(decl: Declaration[Pre]): Unit = decl match { case chor: Choreography[Pre] => @@ -32,7 +38,7 @@ case class DeduplicateChorGuards[Pre <: Generation]() case InChor(_, c @ ChorStatement(loop: Loop[Pre])) => c.rewrite(inner = loop.rewrite(cond = dedup(loop.cond))) - case _ => rewriteDefault(statement) + case _ => statement.rewriteDefault() } def dedup(expr: Expr[Pre]): Expr[Post] = { diff --git a/src/rewrite/vct/rewrite/veymont/GenerateImplementation.scala b/src/rewrite/vct/rewrite/veymont/GenerateImplementation.scala deleted file mode 100644 index 7a0345db0b..0000000000 --- a/src/rewrite/vct/rewrite/veymont/GenerateImplementation.scala +++ /dev/null @@ -1,1087 +0,0 @@ -package vct.rewrite.veymont - -import com.typesafe.scalalogging.LazyLogging -import hre.util.ScopedStack -import vct.col.ast.{ - AbstractRewriter, - ApplicableContract, - Assert, - Assign, - Block, - BooleanValue, - Branch, - ByReferenceClass, - ChorPerm, - ChorRun, - ChorStatement, - Choreography, - Class, - ClassDeclaration, - CommunicateX, - ConstructorInvocation, - Declaration, - Deref, - Endpoint, - EndpointExpr, - EndpointName, - EndpointStatement, - Eval, - Expr, - Fork, - InstanceField, - InstanceMethod, - IterationContract, - JavaClass, - JavaConstructor, - JavaInvocation, - JavaLocal, - JavaMethod, - JavaNamedType, - JavaParam, - JavaPublic, - JavaTClass, - Join, - Local, - Loop, - LoopContract, - LoopInvariant, - MethodInvocation, - NewObject, - Node, - Null, - Perm, - Procedure, - Program, - RunMethod, - Scope, - Star, - Statement, - TClass, - TByReferenceClass, - TVeyMontChannel, - TVoid, - ThisChoreography, - ThisObject, - Type, - UnitAccountedPredicate, - Variable, - VeyMontAssignExpression, -} -import vct.col.origin.{AssignLocalOk, Name, Origin, PanicBlame} -import vct.col.ref.Ref -import vct.col.resolve.ctx.RefJavaMethod -import vct.col.rewrite.adt.ImportADTImporter -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} -import vct.col.util.SuccessionMap -import vct.col.util.AstBuildHelpers._ -import vct.result.VerificationError.{Unreachable, UserError} -import vct.rewrite.veymont.GenerateImplementation.{ - ChannelFieldOrigin, - ParalleliseEndpointsError, - RunMethodOrigin, - ThreadClassOrigin, - getChannelClassName, - getThreadClassName, - getVarName, -} - -import scala.collection.mutable - -object GenerateImplementation extends RewriterBuilder { - override def key: String = "generateImplementation" - - override def desc: String = - "Generate classes for VeyMont threads in parallel program" - - private val channelClassName = "Channel" - private val threadClassName = "Thread" - - def getChannelClassName(channelType: Type[_]): String = - channelType.toString.capitalize + channelClassName - - def getThreadClassName(thread: Endpoint[_]): String = - thread.o.getPreferredNameOrElse().ucamel + threadClassName - - def getVarName(v: Variable[_]) = v.o.getPreferredNameOrElse() - - case class ParalleliseEndpointsError(node: Node[_], msg: String) - extends UserError { - override def code: String = "paralleliseEndpointsError" - override def text: String = node.o.messageInContext(msg) - } - - private def ThreadClassOrigin(thread: Endpoint[_]): Origin = - thread.o.where(name = getThreadClassName(thread)) - - private def ChannelFieldOrigin( - channelName: String, - assign: Statement[_], - ): Origin = assign.o.where(name = channelName) - - private def RunMethodOrigin(runMethod: ChorRun[_]): Origin = - runMethod.o.where(name = "run") -} - -case class GenerateImplementation[Pre <: Generation]() - extends Rewriter[Pre] with LazyLogging { - outer => - - val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = - ScopedStack() - val threadClassSucc: SuccessionMap[Endpoint[Pre], Class[Post]] = - SuccessionMap() - val threadMethodSucc - : SuccessionMap[(Endpoint[Pre], ClassDeclaration[Pre]), InstanceMethod[ - Post - ]] = SuccessionMap() - val runSucc: mutable.LinkedHashMap[Choreography[Pre], Procedure[Post]] = - mutable.LinkedHashMap() - private val givenClassSucc: SuccessionMap[Type[Pre], Class[Post]] = - SuccessionMap() - private val givenClassConstrSucc: SuccessionMap[Type[Pre], Procedure[Pre]] = - SuccessionMap() - val endpointLocals: SuccessionMap[Endpoint[Pre], Variable[Post]] = - SuccessionMap() - - // For each endpoint and input variable, there is a unique instance field (on the class of the endpoint) - val endpointParamFields = - SuccessionMap[(Endpoint[Pre], Variable[Pre]), InstanceField[Post]]() - // For each endpoint and another endpoint, there is a unique instance field (on the class of the endpoint) with a reference to the second endpoint - val endpointPeerFields = - SuccessionMap[(Endpoint[Pre], Endpoint[Pre]), InstanceField[Post]]() - - var program: Program[Pre] = null - lazy val choreographies: Seq[Choreography[Pre]] = program.declarations - .collect { case chor: Choreography[Pre] => chor } - lazy val allEndpoints = choreographies.flatMap { _.endpoints } - lazy val endpointToChoreography: Map[Endpoint[Pre], Choreography[Pre]] = - choreographies.flatMap { chor => chor.endpoints.map(ep => (ep, chor)) } - .toMap - lazy val endpointClassToEndpoint: Map[Class[Pre], Endpoint[Pre]] = - choreographies.flatMap { chor => - chor.endpoints.map(endpoint => (endpoint.cls.decl, endpoint)) - }.toMap - - def isEndpointClass(c: Class[Pre]): Boolean = - endpointClassToEndpoint.contains(c) - def choreographyOf(c: Class[Pre]): Choreography[Pre] = - endpointToChoreography(endpointClassToEndpoint(c)) - def endpointOf(c: Class[Pre]): Endpoint[Pre] = endpointClassToEndpoint(c) - def isChoreographyParam(v: Variable[Pre]): Boolean = - choreographies.exists { chor => chor.params.contains(v) } - - val currentChoreography = ScopedStack[Choreography[Pre]]() - val currentEndpoint = ScopedStack[Endpoint[Pre]]() - - def inChoreography: Boolean = - currentChoreography.nonEmpty && currentEndpoint.isEmpty - def inEndpoint: Boolean = - currentChoreography.nonEmpty && currentEndpoint.nonEmpty - - object InChor { - def unapply[T](t: T): Option[(Choreography[Pre], T)] = - if (inChoreography) - Some((currentChoreography.top, t)) - else - None - def unapply: Option[Choreography[Pre]] = - if (inChoreography) - currentChoreography.topOption - else - None - } - - object InEndpoint { - def unapply[T](t: T): Option[(Choreography[Pre], Endpoint[Pre], T)] = - if (inEndpoint) - Some((currentChoreography.top, currentEndpoint.top, t)) - else - None - def unapply: Option[(Choreography[Pre], Endpoint[Pre])] = - if (inEndpoint) - Some((currentChoreography.top, currentEndpoint.top)) - else - None - } - - val currentThis = ScopedStack[ThisObject[Post]]() - - override def dispatch(program: Program[Pre]): Program[Post] = { - this.program = program - super.dispatch(program) - } - - override def dispatch(decl: Declaration[Pre]): Unit = { - decl match { - case p: Procedure[Pre] => super.dispatch(p) - case cls: ByReferenceClass[Pre] if isEndpointClass(cls) => - val chor = choreographyOf(cls) - val endpoint = endpointOf(cls) - currentThis.having(ThisObject[Post](succ(cls))(cls.o)) { - globalDeclarations.succeed( - cls, - cls.rewrite(decls = - classDeclarations.collect { - cls.decls.foreach(dispatch) - generateRunMethod(chor, endpointOf(cls)) - generateParamFields(chor, endpoint) - generatePeerFields(chor, endpoint) - }._1 - ), - ) - } - case cls: Class[Pre] => super.dispatch(cls) - case chor: Choreography[Pre] => - currentChoreography.having(chor) { - chor.drop() - chor.endpoints.foreach(_.drop()) - implicit val o = chor.o - - chor.endpoints.foreach(endpoint => - endpointLocals(endpoint) = - new Variable(dispatch(endpoint.t))(endpoint.o) - ) - - val initEndpoints = chor.endpoints.map { endpoint => - assignLocal[Post]( - endpointLocals(endpoint).get, - dispatch(endpoint.init), - ) - } - - // Initialize the fields on each endpoint class, representing the parameters of the choreography, and other endpoints - val auxFieldAssigns = chor.endpoints.flatMap { endpoint => - chor.params.map { param => - assignField[Post]( - endpointLocals(endpoint).get, - endpointParamFields.ref((endpoint, param)), - Local(succ(param)), - blame = PanicBlame("Should be safe"), - ) - } ++ chor.endpoints.map { peer => - assignField[Post]( - endpointLocals(endpoint).get, - endpointPeerFields.ref((endpoint, peer)), - endpointLocals(peer).get, - blame = PanicBlame("Should be safe"), - ) - } - } - - val forkJoins = - chor.endpoints.map { endpoint => - Fork[Post](endpointLocals(endpoint).get)(PanicBlame("")) - } ++ chor.endpoints.map { endpoint => - Join[Post](endpointLocals(endpoint).get)(PanicBlame("")) - } - - val mainBody = Scope( - chor.endpoints.map(endpointLocals(_)), - Block( - initEndpoints ++ - Seq(chor.preRun.map(dispatch).getOrElse(Block(Seq()))) ++ - auxFieldAssigns ++ forkJoins - )(chor.o), - ) - - globalDeclarations.declare( - procedure( - args = variables.dispatch(chor.params), - body = Some(mainBody), - blame = PanicBlame("TODO: Procedure"), - contractBlame = PanicBlame("TODO: Procedure contract"), - )(chor.o) - ) - } - case other => rewriteDefault(other) - } - } - - def generateRunMethod( - chor: Choreography[Pre], - endpoint: Endpoint[Pre], - ): Unit = { - val run = chor.run - implicit val o = run.o - currentChoreography.having(chor) { - currentEndpoint.having(endpoint) { - classDeclarations.declare( - new RunMethod( - body = Some(projectStmt(run.body)(endpoint)), - contract = dispatch(run.contract), - )(PanicBlame("")) - ) - } - } - } - - def generateParamFields( - chor: Choreography[Pre], - endpoint: Endpoint[Pre], - ): Unit = - chor.params.foreach { param => - val f = - new InstanceField(dispatch(param.t), Seq())(param.o.where(indirect = - Name.names( - chor.o.getPreferredNameOrElse(), - Name("p"), - param.o.getPreferredNameOrElse(), - ) - )) - classDeclarations.declare(f) - endpointParamFields((endpoint, param)) = f - } - - def generatePeerFields( - chor: Choreography[Pre], - endpoint: Endpoint[Pre], - ): Unit = - chor.endpoints.foreach { peer => - val f = - new InstanceField(dispatch(peer.t), Seq())( - endpoint.o - .where(indirect = Name.names(peer.o.getPreferredNameOrElse())) - ) - classDeclarations.declare(f) - endpointPeerFields((endpoint, peer)) = f - } - - override def dispatch(statement: Statement[Pre]): Statement[Post] = { - if (currentEndpoint.nonEmpty) - projectStmt(statement)(currentEndpoint.top) - else - super.dispatch(statement) - } - - override def dispatch(expr: Expr[Pre]): Expr[Post] = - expr match { - case InChor(_, EndpointName(Ref(endpoint))) => - Local[Post](endpointLocals.ref(endpoint))(expr.o) - case InEndpoint(_, endpoint, EndpointName(Ref(peer))) => - implicit val o = expr.o - // TODO (RR): Also need to generate (read) permissions for all these fields! - Deref[Post](currentThis.top, endpointPeerFields.ref((endpoint, peer)))( - PanicBlame("Shouldn't happen") - ) - case InEndpoint(_, endpoint, Local(Ref(v))) - if currentChoreography.nonEmpty && currentEndpoint.nonEmpty && - isChoreographyParam(v) => - implicit val o = expr.o - Deref[Post](currentThis.top, endpointParamFields.ref((endpoint, v)))( - PanicBlame("Shouldn't happen") - ) - case InEndpoint(_, endpoint, expr) => projectExpr(expr)(endpoint) - case _ => expr.rewriteDefault() - } - - def projectStmt( - statement: Statement[Pre] - )(implicit endpoint: Endpoint[Pre]): Statement[Post] = - statement match { - case EndpointStatement(None, statement) => - statement match { - case _ => - throw new Exception( - "Encountered ChorStatement without endpoint context" - ) - } - case EndpointStatement(Some(Ref(other)), inner) if other == endpoint => - inner match { - case assign: Assign[Pre] => assign.rewriteDefault() - case eval: Eval[Pre] => eval.rewriteDefault() - } - // Ignore statements that do not match the current endpoint - case EndpointStatement(_, _) => Block(Seq())(statement.o) - // Specialize composite statements to the current endpoint - case c @ ChorStatement(branch: Branch[Pre]) - if c.explicitEndpoints.contains(endpoint) => - implicit val o = branch.o - Branch[Post]( - Seq((projectExpr(branch.cond), projectStmt(branch.yes))) ++ - branch.no.map(no => Seq((tt[Post], projectStmt(no)))) - .getOrElse(Seq()) - ) - case c @ ChorStatement(l: Loop[Pre]) - if c.explicitEndpoints.contains(endpoint) => - implicit val o = l.o - loop( - cond = projectExpr(l.cond), - body = projectStmt(l.body), - contract = dispatch(l.contract), - ) - // Ignore loops, branches that the current endpoint doesn't participate in - case c @ ChorStatement(_: Loop[Pre] | _: Branch[Pre]) => Block(Seq())(c.o) - // Rewrite blocks transparently - case block: Block[Pre] => block.rewriteDefault() - // Don't let any missed cases slip through - case s => throw new Exception(s"Unsupported: $s") - } - - def projectContract( - contract: LoopContract[Pre] - )(implicit endpoint: Endpoint[Pre]): LoopContract[Post] = - contract match { - case inv: LoopInvariant[Pre] => - inv.rewrite(invariant = projectExpr(inv.invariant)) - case it: IterationContract[Pre] => - it.rewrite( - requires = projectExpr(it.requires), - ensures = projectExpr(it.ensures), - ) - } - - def projectContract( - contract: ApplicableContract[Pre] - )(implicit endpoint: Endpoint[Pre]): ApplicableContract[Post] = - contract.rewrite( - requires = (projectExpr(_)).accounted(contract.requires), - ensures = (projectExpr(_)).accounted(contract.ensures), - contextEverywhere = projectExpr(contract.contextEverywhere), - ) - - def projectExpr( - expr: Expr[Pre] - )(implicit endpoint: Endpoint[Pre]): Expr[Post] = - expr match { - case ChorPerm(Ref(other), loc, perm) if endpoint == other => - Perm(dispatch(loc), dispatch(perm))(expr.o) - case ChorPerm(Ref(other), _, _) if endpoint != other => tt - case EndpointExpr(Ref(other), expr) if endpoint == other => - projectExpr(expr) - case EndpointExpr(Ref(other), expr) => tt - case _ => expr.rewriteDefault() - } - - // - // Old code after this - // - - private def dispatchThread(thread: Endpoint[Pre]): Unit = { - if (threadBuildingBlocks.nonEmpty) { - val threadRes: ThreadBuildingBlocks[Pre] = threadBuildingBlocks.top - val threadMethods: Seq[ClassDeclaration[Post]] = createThreadMethod( - thread, - threadRes, - ) - createThreadClass(thread, threadRes, threadMethods) - } else - rewriteDefault(thread) - } - - private def dispatchThreads(seqProg: Choreography[Pre]): Unit = { - val (channelClasses, indexedChannelInfo) = extractChannelInfo(seqProg) - channelClasses.foreach { case (t, c) => globalDeclarations.declare(c) } - seqProg.endpoints.foreach(thread => { - val threadField = - new InstanceField[Post]( - TByReferenceClass(givenClassSucc.ref(thread.t), Seq()), - Nil, - )(thread.o) - val channelFields = getChannelFields( - thread, - indexedChannelInfo, - channelClasses, - ) - threadBuildingBlocks.having(new ThreadBuildingBlocks( - seqProg.run, - seqProg.decls, - channelFields, - channelClasses, - thread, - threadField, - )) { dispatch(thread) } - }) - } - - private def dispatchGivenClass(c: ByReferenceClass[Pre]): Class[Post] = { - val rw = GivenClassRewriter() - val gc = - c.rewrite(decls = - classDeclarations.collect { - (givenClassConstrSucc.get(TByReferenceClass(c.ref, Seq())).get +: - c.declarations).foreach(d => rw.dispatch(d)) - }._1 - )(rw) - givenClassSucc.update(TByReferenceClass(c.ref, Seq()), gc) - gc - } - - case class GivenClassRewriter() extends Rewriter[Pre] { - override val allScopes = outer.allScopes - - val rewritingConstr: ScopedStack[(Seq[Variable[Pre]], TClass[Pre])] = - ScopedStack() - - override def dispatch(decl: Declaration[Pre]): Unit = - decl match { - case p: Procedure[Pre] => - p.returnType match { - case tc: TClass[Pre] => - rewritingConstr.having(p.args, tc) { - classDeclarations.declare(createClassConstructor(p)) - }; - case _ => - ??? // ("This procedure is expected to have a class as return type"); - } - case other => rewriteDefault(other) - } - - // PB: from what I understand this restores a constructor from a generated procedure, so this should be refactored - // once we make constructors first class. - def createClassConstructor(p: Procedure[Pre]): JavaConstructor[Post] = - new JavaConstructor[Post]( - Seq(JavaPublic[Post]()(p.o)), - rewritingConstr.top._2.cls.decl.o.getPreferredNameOrElse().ucamel, - p.args.map(createJavaParam), - variables.dispatch(p.typeArgs), - Seq.empty, - p.body match { - case Some(s: Scope[Pre]) => - s.body match { - case b: Block[Pre] => - dispatch(Block(b.statements.tail.dropRight(1))(p.o)) - case other => dispatch(other) - } - case Some(_) => - throw Unreachable( - "The body of a procedure always starts with a Scope." - ) - case None => Block(Seq.empty)(p.o) - }, - p.contract.rewrite(ensures = - UnitAccountedPredicate[Post](BooleanValue(true)(p.o))(p.o) - ), - )(null)(p.o) - - def createJavaParam(v: Variable[Pre]): JavaParam[Post] = - new JavaParam[Post](Seq.empty, getVarName(v).camel, dispatch(v.t))(v.o) - - override def dispatch(e: Expr[Pre]): Expr[Post] = - e match { - case l: Local[Pre] => - if ( - rewritingConstr.nonEmpty && - rewritingConstr.top._1.contains(l.ref.decl) - ) - JavaLocal[Post](getVarName(l.ref.decl).camel)(null)(e.o) - else - rewriteDefault(l) - case t: ThisObject[Pre] => - val thisClassType = TByReferenceClass(t.cls, Seq()) - if ( - rewritingConstr.nonEmpty && rewritingConstr.top._2 == thisClassType - ) - ThisObject(givenClassSucc.ref[Post, Class[Post]](thisClassType))( - t.o - ) - else - rewriteDefault(t) - case d: Deref[Pre] => - if (rewritingConstr.nonEmpty) - d.obj match { - case _: Local[Pre] => - d.rewrite(obj = - ThisObject( - givenClassSucc - .ref[Post, Class[Post]](rewritingConstr.top._2) - )(d.o) - ) - case other => rewriteDefault(other) - } - else - rewriteDefault(d) - case other => rewriteDefault(other) - } - } - - private def extractChannelInfo( - seqProg: Choreography[Pre] - ): (Map[Type[Pre], JavaClass[Post]], Seq[ChannelInfo[Pre]]) = { - val channelInfo = - getChannelNamesAndTypes(seqProg.run.body) ++ - collectChannelsFromMethods(seqProg) - val indexedChannelInfo: Seq[ChannelInfo[Pre]] = - channelInfo.groupBy(_.channelName).values.flatMap(chanInfoSeq => - if (chanInfoSeq.size <= 1) - chanInfoSeq - else - chanInfoSeq.zipWithIndex.map { case (chanInfo, index) => - new ChannelInfo( - chanInfo.comExpr, - chanInfo.channelType, - chanInfo.channelName + index, - ) - } - ).toSeq - val channelClasses = generateChannelClasses(indexedChannelInfo) - (channelClasses, indexedChannelInfo) - } - - private def createThreadMethod( - thread: Endpoint[Pre], - threadRes: ThreadBuildingBlocks[Pre], - ) = { - threadRes.methods.map { preMethod => - val postMethod = getThreadMethodFromDecl(thread)(preMethod) - threadMethodSucc.update((thread, preMethod), postMethod) - postMethod - } - } - - private def createThreadClass( - thread: Endpoint[Pre], - threadRes: ThreadBuildingBlocks[Pre], - threadMethods: Seq[ClassDeclaration[Post]], - ): Unit = { - val threadConstr = createThreadClassConstructor( - thread, - threadRes.threadField, - ) - val threadRun = getThreadRunMethod(threadRes.runMethod) - classDeclarations.scope { - val threadClass = - new ByReferenceClass[Post]( - Seq(), - (threadRes.threadField +: threadRes.channelFields.values.toSeq) ++ - (threadConstr +: threadRun +: threadMethods), - Seq(), - BooleanValue(true)(thread.o), - )(ThreadClassOrigin(thread)) - globalDeclarations.declare(threadClass) - threadClassSucc.update(thread, threadClass) - } - } - - private def createThreadClassConstructor( - thread: Endpoint[Pre], - threadField: InstanceField[Post], - ): JavaConstructor[Post] = { - val threadConstrArgBlocks: Seq[(Name, Type[Post])] = - ??? /* thread.args.map { - case l: Local[Pre] => - (l.ref.decl.o.getPreferredNameOrElse(), dispatch(l.t)) - case other => - throw ParalleliseEndpointsError( - other, - "This node is expected to be an argument of seq_prog, and have type Local", - ) - } */ - val threadConstrArgs: Seq[JavaParam[Post]] = threadConstrArgBlocks.map { - case (a, t) => - new JavaParam[Post](Seq.empty, a.camel, t)(ThreadClassOrigin(thread)) - } - val passedArgs = threadConstrArgs - .map(a => JavaLocal[Post](a.name)(null)(ThreadClassOrigin(thread))) - // TODO: The next check cannot fail anymore - val threadTypeName = - thread.t match { // TODO: replace by using givenClassSucc - case tc: TClass[Pre] => tc.cls.decl.o.getPreferredNameOrElse() - case _ => - throw ParalleliseEndpointsError( - thread, - "This type is expected to be a class", - ) - } - val threadConstrBody = { - Assign( - getThisVeyMontDeref(thread, ThreadClassOrigin(thread), threadField), - JavaInvocation[Post]( - None, - Seq.empty, - "new " + threadTypeName.ucamel, - passedArgs, - Seq.empty, - Seq.empty, - )(null)(ThreadClassOrigin(thread)), - )(null)(ThreadClassOrigin(thread)) - } - val threadConstrContract = - new ApplicableContract[Post]( - UnitAccountedPredicate[Post]( - BooleanValue(true)(ThreadClassOrigin(thread)) - )(ThreadClassOrigin(thread)), - UnitAccountedPredicate[Post]( - BooleanValue(true)(ThreadClassOrigin(thread)) - )(ThreadClassOrigin(thread)), - BooleanValue(true)(ThreadClassOrigin(thread)), - Seq.empty, - Seq.empty, - Seq.empty, - None, - )(null)(ThreadClassOrigin(thread)) - new JavaConstructor[Post]( - Seq(JavaPublic[Post]()(ThreadClassOrigin(thread))), - getThreadClassName(thread), - threadConstrArgs, - Seq.empty, - Seq.empty, - threadConstrBody, - threadConstrContract, - )(ThreadClassOrigin(thread))(ThreadClassOrigin(thread)) - } - - private def getThreadMethodFromDecl( - thread: Endpoint[Pre] - )(decl: ClassDeclaration[Pre]): InstanceMethod[Post] = - decl match { - case m: InstanceMethod[Pre] => getThreadMethod(m) - case _ => - throw ParalleliseEndpointsError( - thread, - "Methods of seq_program need to be of type InstanceMethod", - ) - } - - private def getChannelFields( - thread: Endpoint[Pre], - channelInfo: Seq[ChannelInfo[Pre]], - channelClasses: Map[Type[Pre], JavaClass[Post]], - ): Map[(CommunicateX[Pre], Origin), InstanceField[Post]] = { - channelInfo.filter(chanInfo => - chanInfo.comExpr.receiver.decl == thread || - chanInfo.comExpr.sender.decl == thread - ).map { chanInfo => - val chanFieldOrigin = ChannelFieldOrigin( - chanInfo.channelName, - chanInfo.comExpr.assign, - ) - val chanField = - new InstanceField[Post]( - TVeyMontChannel(getChannelClassName(chanInfo.channelType)), - Nil, - )(chanFieldOrigin) - ((chanInfo.comExpr, chanInfo.comExpr.o), chanField) - }.toMap - } - - private def generateChannelClasses( - channelInfo: Seq[ChannelInfo[Pre]] - ): Map[Type[Pre], JavaClass[Post]] = { - val channelTypes = channelInfo.map(_.channelType).toSet - channelTypes.map(channelType => - channelType -> { - val chanClassPre = ( /* channelClass */ ???) - .asInstanceOf[JavaClass[Pre]] - val rw = ChannelClassGenerator(channelType) - chanClassPre.rewrite( - name = getChannelClassName(channelType), - modifiers = Seq.empty, - decls = - classDeclarations.collect { - chanClassPre.decls.foreach(d => rw.dispatch(d)) - }._1, - )(rw) - } - ).toMap - } - - case class ChannelClassGenerator(channelType: Type[_]) extends Rewriter[Pre] { - override val allScopes = outer.allScopes - - override def dispatch(t: Type[Pre]): Type[Post] = - t match { - case jnt: JavaNamedType[Pre] => - if (jnt.names.head._1 == "MessageType") { - dispatch(channelType.asInstanceOf[Type[Pre]]) - } else - rewriteDefault(jnt) - case _ => rewriteDefault(t) - } - - override def dispatch(decl: Declaration[Pre]): Unit = - decl match { - case jc: JavaConstructor[Pre] => - classDeclarations - .declare(jc.rewrite(name = getChannelClassName(channelType))) - case other => rewriteDefault(other) - } - } - - private def collectChannelsFromMethods(seqProg: Choreography[Pre]) = - seqProg.decls.flatMap { - case m: InstanceMethod[Pre] => - m.body.map(getChannelNamesAndTypes).getOrElse( - throw ParalleliseEndpointsError( - m, - "Abstract methods are not supported inside a choreography.", - ) - ) - case other => - throw ParalleliseEndpointsError(other, "choreography method expected") - } - - private def getChannelNamesAndTypes( - s: Statement[Pre] - ): Seq[ChannelInfo[Pre]] = { - s.collect { case e @ CommunicateX(recv, sender, chanType, assign) => - new ChannelInfo( - e, - chanType, - recv.decl.o.getPreferredNameOrElse().ucamel + - sender.decl.o.getPreferredNameOrElse().camel + "Channel", - ) - } - } - - private def getThreadMethod( - method: InstanceMethod[Pre] - ): InstanceMethod[Post] = { - new InstanceMethod[Post]( - dispatch(method.returnType), - variables.dispatch(method.args), - variables.dispatch(method.outArgs), - variables.dispatch(method.typeArgs), - method.body.map(dispatch), - dispatch(method.contract), - )(method.blame)(method.o) - } - - private def getThreadRunMethod(run: ChorRun[Pre]): InstanceMethod[Post] = { - new InstanceMethod[Post]( - TVoid[Post](), - Seq.empty, - Seq.empty, - Seq.empty, - Some(dispatch(run.body)), - dispatch(run.contract), - )(PanicBlame( - "TODO: Convert InstanceMethod blame to SeqRun blame" - ) /* run.blame */ )(RunMethodOrigin(run)) - } - - def dispatchExpr(node: Expr[Pre]): Expr[Post] = { - if (threadBuildingBlocks.nonEmpty) { - val thread = threadBuildingBlocks.top.thread - node match { - // 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: EndpointName[Pre] => - updateThreadRefVeyMontDeref(node, thread, t) - case _ => rewriteDefault(node) - } - } else - rewriteDefault(node) - } - - private def updateThreadRefVeyMontDeref( - node: Expr[Pre], - thread: Endpoint[Pre], - t: EndpointName[Pre], - ) = { - if (t.ref.decl == thread) { - getThisVeyMontDeref(thread, t.o, threadBuildingBlocks.top.threadField) - } else - rewriteDefault(node) - } - - private def updateThreadRefInDeref( - node: Expr[Pre], - thread: Endpoint[Pre], - d: Deref[Pre], - ) = { - d.obj match { - case t: EndpointName[Pre] if t.ref.decl == thread => - d.rewrite(obj = - getThisVeyMontDeref(thread, d.o, threadBuildingBlocks.top.threadField) - ) - case _ => rewriteDefault(node) - } - } - - private def updateThreadRefMethodInvoc( - thread: Endpoint[Pre], - m: MethodInvocation[Pre], - ) = { - m.obj match { - case threadRef: EndpointName[Pre] => - ??? // m.rewrite(obj = EndpointNameExpr(dispatch(threadRef))) - case _ => - threadMethodSucc.get((thread, m.ref.decl)) match { - case Some(postMethod) => - m.rewrite( - obj = dispatch(m.obj), - ref = postMethod.ref[InstanceMethod[Post]], - m.args.map(dispatch), - ) - case None => - throw ParalleliseEndpointsError( - m, - "No successor for this method found", - ) - } - } - } - -// private def paralleliseThreadCondition( -// node: Expr[Pre], -// thread: Endpoint[Pre], -// c: ChorGuard[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]], - ) = { - Deref( - ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), - threadField.ref[InstanceField[Post]], - )(null)(o) - } - - def dispatchStatement(st: Statement[Pre]): Statement[Post] = { - if (threadBuildingBlocks.nonEmpty) { - val thread = threadBuildingBlocks.top.thread - st match { - case v: CommunicateX[Pre] => - paralleliseVeyMontCommExpr(thread, v, createParComBlocks(thread, v)) - case v @ VeyMontAssignExpression(threadRef, assign) => - if (threadRef.decl == thread) - dispatch(assign) - else - Block(Seq.empty)(assign.o) - case a: Assign[Pre] => - Assign(dispatch(a.target), dispatch(a.value))(a.blame)(a.o) - case Branch(_) => rewriteDefault(st) - case Loop(_, _, _, _, _) => rewriteDefault(st) - case Scope(_, _) => rewriteDefault(st) - case Block(_) => rewriteDefault(st) - case Eval(expr) => paralleliseMethodInvocation(st, thread, expr) - case _: Assert[Pre] => Block(Seq.empty)(st.o) - case _ => - throw ParalleliseEndpointsError( - st, - "Statement not allowed in choreography", - ) - } - } else - rewriteDefault(st) - } - - private def createParComBlocks( - thread: Endpoint[Pre], - v: CommunicateX[Pre], - ): ParallelCommExprBuildingBlocks[Pre] = { - val channelField = threadBuildingBlocks.top.channelFields((v, v.o)) - val channelClass = threadBuildingBlocks.top.channelClasses(v.chanType) - val thisChanField = - Deref( - ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), - channelField.ref[InstanceField[Post]], - )(null)(v.assign.o) - val assignment = v.assign.asInstanceOf[Assign[Pre]] - new ParallelCommExprBuildingBlocks( - channelField, - channelClass, - thisChanField, - assignment, - ) - } - - private def paralleliseMethodInvocation( - st: Statement[Pre], - thread: Endpoint[Pre], - expr: Expr[Pre], - ): Statement[Post] = { - expr match { - case m: MethodInvocation[Pre] => - m.obj match { - case _: ThisChoreography[Pre] => - Eval(m.rewrite( - obj = - ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))( - thread.o - ), - ref = threadMethodSucc - .ref[Post, InstanceMethod[Post]]((thread, m.ref.decl)), - ))(st.o) -// case EndpointNameExpr(d: EndpointName[Pre]) => ??? // if (d.ref.decl == thread) Eval(dispatch(expr))(st.o) else Block(Seq.empty)(st.o) - case _ => - throw ParalleliseEndpointsError( - st, - "Statement not allowed in seq_program", - ) - } - case _ => - throw ParalleliseEndpointsError( - st, - "Statement not allowed in seq_program", - ) - } - } - - private def paralleliseVeyMontCommExpr( - thread: Endpoint[Pre], - v: CommunicateX[Pre], - blocks: ParallelCommExprBuildingBlocks[Pre], - ): Statement[Post] = { - if (v.receiver.decl == thread) { - val readMethod = findChannelClassMethod( - v, - blocks.channelClass, - "readValue", - ) - val assignValue = - JavaInvocation( - Some(blocks.thisChanField), - Seq.empty, - "readValue", - Seq.empty, - Seq.empty, - Seq.empty, - )(null)(v.o) - assignValue.ref = Some(RefJavaMethod(readMethod)) - Assign(dispatch(blocks.assign.target), assignValue)(null)(v.o) - } else if (v.sender.decl == thread) { - val writeMethod = findChannelClassMethod( - v, - blocks.channelClass, - "writeValue", - ) - val writeInvoc = - JavaInvocation( - Some(blocks.thisChanField), - Seq.empty, - "writeValue", - Seq(dispatch(blocks.assign.value)), - Seq.empty, - Seq.empty, - )(null)(v.o) - writeInvoc.ref = Some(RefJavaMethod(writeMethod)) - Eval(writeInvoc)(v.o) - } else - Block(Seq.empty)(blocks.assign.o) - } - - private def findChannelClassMethod( - v: CommunicateX[Pre], - channelClass: JavaClass[Post], - methodName: String, - ): JavaMethod[Post] = { - val method = channelClass.decls.find { - case jm: JavaMethod[Post] => jm.name == methodName - case _ => false - } - method match { - case Some(m: JavaMethod[Post]) => m - case _ => - throw ParalleliseEndpointsError( - v, - "Could not find method `" + methodName + "' for channel class " + - channelClass.name, - ) - } - } - -} diff --git a/src/rewrite/vct/rewrite/veymont/InferEndpointContexts.scala b/src/rewrite/vct/rewrite/veymont/InferEndpointContexts.scala index 3fa43055af..f1f7faa1fe 100644 --- a/src/rewrite/vct/rewrite/veymont/InferEndpointContexts.scala +++ b/src/rewrite/vct/rewrite/veymont/InferEndpointContexts.scala @@ -76,15 +76,6 @@ import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} import vct.col.util.SuccessionMap import vct.col.util.AstBuildHelpers._ import vct.result.VerificationError.{SystemError, Unreachable, UserError} -import vct.rewrite.veymont.GenerateImplementation.{ - ChannelFieldOrigin, - ParalleliseEndpointsError, - RunMethodOrigin, - ThreadClassOrigin, - getChannelClassName, - getThreadClassName, - getVarName, -} import vct.rewrite.veymont.InferEndpointContexts.{ EndpointInferenceUndefined, MultipleImplicitEndpointsError, @@ -178,6 +169,8 @@ case class InferEndpointContexts[Pre <: Generation]() s.rewrite(endpoint = Some(succ(endpoint))) case s @ EndpointStatement(None, _) => throw EndpointInferenceUndefined(s) case comm: CommunicateStatement[Pre] => + // Make inChor false because we don't want to infer endpoint contexts for expressions in the channel invariant + // These should remain plain inChor.having(false) { comm.rewriteDefault() } case s => s.rewriteDefault() } diff --git a/src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala deleted file mode 100644 index 06bf399cde..0000000000 --- a/src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala +++ /dev/null @@ -1,11 +0,0 @@ -package vct.rewrite.veymont - -import vct.col.ast.{Assign, Deref, InstanceField, JavaClass} -import vct.col.rewrite.{Generation, Rewritten} - -class ParallelCommExprBuildingBlocks[Pre <: Generation]( - val channelField: InstanceField[Rewritten[Pre]], - val channelClass: JavaClass[Rewritten[Pre]], - val thisChanField: Deref[Rewritten[Pre]], - val assign: Assign[Pre], -) {} diff --git a/src/rewrite/vct/rewrite/veymont/StratifyExpressions.scala b/src/rewrite/vct/rewrite/veymont/StratifyExpressions.scala index c19e42e691..5d6c7632fa 100644 --- a/src/rewrite/vct/rewrite/veymont/StratifyExpressions.scala +++ b/src/rewrite/vct/rewrite/veymont/StratifyExpressions.scala @@ -35,10 +35,13 @@ case class StratifyExpressions[Pre <: Generation]() extends Rewriter[Pre] with VeymontContext[Pre] with LazyLogging { override def dispatch(prog: Program[Pre]): Program[Post] = { + mappings.program = prog + val newProg = prog.rewrite() val errors = newProg.check - // TODO (RR): if we refactor branches to be nested instead of flat, this check can - // happen directly after LangVeyMontToCol + /* TODO (RR): if we refactor branches to be nested instead of flat, this check can + happen directly after LangVeyMontToCol. Or we should consider putting the flattening in its own pass, + which then also contains the below check */ val seqBranchErrors = errors.collect { case err: SeqProgParticipant => err } if (errors.nonEmpty && errors.length == seqBranchErrors.length) { throw SeqProgParticipantErrors(seqBranchErrors) @@ -97,15 +100,16 @@ case class StratifyExpressions[Pre <: Generation]() branch .rewrite(Seq((stratifyExpr(cond), dispatch(yes)), (tt, dispatch(no)))) + // We expect all branches to be normalized to binary branches case InChor(_, Branch(_)) => ??? - case assert: Assert[Pre] => + case InChor(_, assert: Assert[Pre]) => assert.rewrite(res = stratifyExpr(assert.expr)) - case inhale: Inhale[Pre] => + case InChor(_, inhale: Inhale[Pre]) => inhale.rewrite(res = stratifyExpr(inhale.expr)) - case exhale: Exhale[Pre] => + case InChor(_, exhale: Exhale[Pre]) => exhale.rewrite(res = stratifyExpr(exhale.expr)) - case assume: Assume[Pre] => + case InChor(_, assume: Assume[Pre]) => assume.rewrite(assn = stratifyExpr(assume.expr)) case statement => statement.rewriteDefault() diff --git a/src/rewrite/vct/rewrite/veymont/StratifyUnpointedExpressions.scala b/src/rewrite/vct/rewrite/veymont/StratifyUnpointedExpressions.scala index 5cb41c921f..7919f53244 100644 --- a/src/rewrite/vct/rewrite/veymont/StratifyUnpointedExpressions.scala +++ b/src/rewrite/vct/rewrite/veymont/StratifyUnpointedExpressions.scala @@ -1,6 +1,7 @@ package vct.rewrite.veymont import hre.util.ScopedStack +import vct.col import vct.col.ast._ import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.util.AstBuildHelpers._ @@ -17,6 +18,11 @@ case class StratifyUnpointedExpressions[Pre <: Generation]() extends Rewriter[Pre] with VeymontContext[Pre] { val currentParticipants: ScopedStack[ListSet[Endpoint[Pre]]] = ScopedStack() + override def dispatch(p: Program[Pre]): Program[Post] = { + mappings.program = p + super.dispatch(p) + } + override def dispatch(decl: Declaration[Pre]): Unit = decl match { case chor: Choreography[Pre] => @@ -87,6 +93,15 @@ case class StratifyUnpointedExpressions[Pre <: Generation]() c.rewrite(inner = loop.rewrite(cond = stratifyExpr(loop.cond))) } + case InChor(_, c @ ChorStatement(assert: Assert[Pre])) => + c.rewrite(inner = assert.rewrite(res = stratifyExpr(assert.res))) + case InChor(_, c @ ChorStatement(assume: Assume[Pre])) => + c.rewrite(inner = assume.rewrite(assn = stratifyExpr(assume.assn))) + case InChor(_, c @ ChorStatement(inhale: Inhale[Pre])) => + c.rewrite(inner = inhale.rewrite(res = stratifyExpr(inhale.res))) + case InChor(_, c @ ChorStatement(exhale: Exhale[Pre])) => + c.rewrite(inner = exhale.rewrite(res = stratifyExpr(exhale.res))) + case statement => statement.rewriteDefault() } diff --git a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala deleted file mode 100644 index c457377b9d..0000000000 --- a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala +++ /dev/null @@ -1,131 +0,0 @@ -package vct.col.rewrite.veymont - -import hre.util.ScopedStack -import vct.col.ast._ -import vct.col.rewrite.veymont.StructureCheck.VeyMontStructCheckError -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} -import vct.result.VerificationError.UserError - -object StructureCheck extends RewriterBuilder { - - override def key: String = "structureCheck" - - override def desc: String = - "Check if program adheres to syntax of VeyMont input program" - - case class VeyMontStructCheckError(node: Node[_], msg: String) - extends UserError { // SystemErrir fir unreachable errros - override def code: String = "veyMontStructCheckError" - - override def text: String = node.o.messageInContext(msg) - } - -} - -case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] { - - val inSeqProg: ScopedStack[Unit] = ScopedStack() - - override def dispatch(decl: Declaration[Pre]): Unit = - decl match { - case dcl: Choreography[Pre] => - inSeqProg.having(()) { rewriteDefault(dcl) } - case m: InstanceMethod[Pre] => - if (inSeqProg.nonEmpty && m.args.nonEmpty) - throw VeyMontStructCheckError( - m, - "Methods in seq_program cannot have any arguments!", - ) - else if (inSeqProg.nonEmpty && m.returnType != TVoid[Pre]()) - throw VeyMontStructCheckError( - m, - "Methods in seq_program cannot have a non-void return type!", - ) - else - rewriteDefault(decl) - case r: RunMethod[Pre] => - if (r.body.isEmpty) - throw VeyMontStructCheckError( - r, - "Method run in seq_program needs to have a body!", - ) - else - rewriteDefault(decl) - case _ => rewriteDefault(decl) - } - - override def dispatch(prog: Program[Pre]): Program[Post] = { - if ( - !prog.declarations.exists { - case dcl: Choreography[Pre] => - if (dcl.endpoints.isEmpty) - throw VeyMontStructCheckError( - dcl, - "A seq_program needs to have at least 1 thread, but none was found!", - ) - else - true - case _ => false - } - ) - throw VeyMontStructCheckError( - prog, - "VeyMont requires a seq_program, but none was found!", - ) - else - rewriteDefault(prog) - } - - override def dispatch(st: Statement[Pre]): Statement[Post] = { - if (inSeqProg.nonEmpty) - st match { - case CommunicateX(_, _, _, _) => rewriteDefault(st) - case VeyMontAssignExpression(_, _) => rewriteDefault(st) - case Assign(_, _) => rewriteDefault(st) - case Branch(_) => rewriteDefault(st) - case Loop(_, _, _, _, _) => rewriteDefault(st) - case Scope(_, _) => rewriteDefault(st) - case Block(_) => rewriteDefault(st) - case Eval(expr) => checkMethodCall(st, expr) - case Assert(_) => rewriteDefault(st) - case _ => - throw VeyMontStructCheckError( - st, - "Statement not allowed in seq_program", - ) - } - else - rewriteDefault(st) - } - - private def checkMethodCall( - st: Statement[Pre], - expr: Expr[Pre], - ): Statement[Post] = { - expr match { - case MethodInvocation(obj, _, args, _, _, _, _) => - obj match { - case ThisChoreography(_) => - if (args.isEmpty) - rewriteDefault(st) - else - throw VeyMontStructCheckError( - st, - "Calls to methods in seq_program cannot have any arguments!", - ) -// case EndpointName(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/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala deleted file mode 100644 index 4b7bb0a44c..0000000000 --- a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala +++ /dev/null @@ -1,24 +0,0 @@ -package vct.rewrite.veymont - -import vct.col.ast.{ - ClassDeclaration, - CommunicateX, - Endpoint, - InstanceField, - JavaClass, - ChorRun, - Type, -} -import vct.col.origin.Origin -import vct.col.rewrite.{Generation, Rewritten} - -class ThreadBuildingBlocks[Pre <: Generation]( - val runMethod: ChorRun[Pre], - val methods: Seq[ClassDeclaration[Pre]], - val channelFields: Map[(CommunicateX[Pre], Origin), InstanceField[ - Rewritten[Pre] - ]], - val channelClasses: Map[Type[Pre], JavaClass[Rewritten[Pre]]], - val thread: Endpoint[Pre], - val threadField: InstanceField[Rewritten[Pre]], -) {} diff --git a/src/rewrite/vct/rewrite/veymont/VeymontContext.scala b/src/rewrite/vct/rewrite/veymont/VeymontContext.scala index cc51913ccb..4152b732b1 100644 --- a/src/rewrite/vct/rewrite/veymont/VeymontContext.scala +++ b/src/rewrite/vct/rewrite/veymont/VeymontContext.scala @@ -2,20 +2,28 @@ package vct.rewrite.veymont import hre.util.ScopedStack import vct.col.ast.{ - Choreography, ChorRun, + Choreography, Class, Communicate, + Constructor, Endpoint, Program, Variable, } -import vct.col.rewrite.Generation +import vct.col.rewrite.{Generation, Rewriter} trait VeymontContext[Pre <: Generation] { + object mappings { var program: Program[Pre] = null + lazy val choreographies: Seq[Choreography[Pre]] = + mappings.program.collect { case c: Choreography[Pre] => c }.toIndexedSeq + + lazy val classes: Seq[Class[Pre]] = + mappings.program.collect { case cls: Class[Pre] => cls }.toIndexedSeq + lazy val choreographyToCommunicates : Map[Choreography[Pre], Seq[Communicate[Pre]]] = choreographies.map { c => @@ -31,10 +39,12 @@ trait VeymontContext[Pre <: Generation] { choreographies.flatMap { chor => chor.endpoints.map(endpoint => (endpoint.cls.decl, endpoint)) }.toMap - } - lazy val choreographies: Seq[Choreography[Pre]] = - mappings.program.collect { case c: Choreography[Pre] => c }.toIndexedSeq + lazy val constructorToClass: Map[Constructor[Pre], Class[Pre]] = + classes.flatMap { cls => + cls.collect { case cons: Constructor[Pre] => (cons, cls) } + }.toMap + } def communicatesOf(chor: Choreography[Pre]) = mappings.choreographyToCommunicates(chor) @@ -55,7 +65,12 @@ trait VeymontContext[Pre <: Generation] { mappings.endpointClassToEndpoint(c) def endpointsOf(run: ChorRun[Pre]) = choreographyOf(run).endpoints def isChoreographyParam(v: Variable[Pre]): Boolean = - choreographies.exists { chor => chor.params.contains(v) } + mappings.choreographies.exists { chor => chor.params.contains(v) } + + def classOf(cons: Constructor[Pre]): Class[Pre] = + mappings.constructorToClass(cons) + def classOfOpt(cons: Constructor[Pre]): Option[Class[Pre]] = + mappings.constructorToClass.get(cons) val currentChoreography = ScopedStack[Choreography[Pre]]() val currentEndpoint = ScopedStack[Endpoint[Pre]]() diff --git a/src/rewrite/vct/rewrite/veymont/DropChorExpr.scala b/src/rewrite/vct/rewrite/veymont/generation/DropChorExpr.scala similarity index 93% rename from src/rewrite/vct/rewrite/veymont/DropChorExpr.scala rename to src/rewrite/vct/rewrite/veymont/generation/DropChorExpr.scala index f24024ca79..f2d1629739 100644 --- a/src/rewrite/vct/rewrite/veymont/DropChorExpr.scala +++ b/src/rewrite/vct/rewrite/veymont/generation/DropChorExpr.scala @@ -1,4 +1,4 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.generation import com.typesafe.scalalogging.LazyLogging import vct.col.ast._ diff --git a/src/rewrite/vct/rewrite/veymont/generation/EncodeGlobalApplicables.scala b/src/rewrite/vct/rewrite/veymont/generation/EncodeGlobalApplicables.scala new file mode 100644 index 0000000000..4ddfe8e7ae --- /dev/null +++ b/src/rewrite/vct/rewrite/veymont/generation/EncodeGlobalApplicables.scala @@ -0,0 +1,215 @@ +package vct.rewrite.veymont.generation + +import hre.util.ScopedStack +import vct.col.ast.{ + ApplicableContract, + Block, + Assert, + Assume, + ByReferenceClass, + Class, + Constructor, + Declaration, + Exhale, + Expr, + Function, + FunctionInvocation, + Inhale, + InstanceFunction, + InstanceFunctionInvocation, + InstanceMethod, + InvokingNode, + LoopContract, + MethodInvocation, + NewObject, + Null, + Procedure, + ProcedureInvocation, + Program, + Result, + Statement, + TByReferenceClass, +} +import vct.col.origin.{ + Blame, + InstanceInvocationFailure, + InstanceNull, + InvocationFailure, + Origin, + PanicBlame, + TrueSatisfiable, +} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ +import vct.col.util.{DeclarationBox, SuccessionMap} +import vct.rewrite.veymont.generation.EncodeGlobalApplicables.InstanceInvocationFailureToInvocationFailure + +object EncodeGlobalApplicables extends RewriterBuilder { + + override def key: String = "encodeGlobalApplicables" + + override def desc: String = + "Encode all global applicables into a class, which is created whenever a global applicable is called." + + case class InstanceInvocationFailureToInvocationFailure(inv: InvokingNode[_]) + extends Blame[InstanceInvocationFailure] { + override def blame(error: InstanceInvocationFailure): Unit = + error match { + case InstanceNull(_) => + PanicBlame("Invocation target guaranteed not to be null") + case failure: InvocationFailure => inv.blame.blame(failure) + } + } +} + +case class EncodeGlobalApplicables[Pre <: Generation]() extends Rewriter[Pre] { + val procSucc = SuccessionMap[Procedure[Pre], InstanceMethod[Post]]() + val funcSucc = SuccessionMap[Function[Pre], InstanceFunction[Post]]() + + val inSpec = ScopedStack[Boolean]() + val globalsConstructor = DeclarationBox[Post, Constructor[Post]]() + val globals = DeclarationBox[Post, Class[Post]]() + val ghostGlobals = DeclarationBox[Post, Function[Post]]() + + def spec[T](f: => T): T = inSpec.having(true) { f } + + def getGlobals(implicit o: Origin): Expr[Post] = + if (inSpec.topOption.contains(true)) + functionInvocation( + ref = ghostGlobals.ref, + blame = PanicBlame("Trivial contract"), + ) + else + constructorInvocation( + ref = globalsConstructor.ref, + blame = PanicBlame("Trivial contract"), + ) + + override def dispatch(expr: Expr[Pre]): Expr[Post] = + expr match { + case inv: ProcedureInvocation[Pre] => + implicit val o = inv.o + MethodInvocation[Post]( + getGlobals, + procSucc.ref(inv.ref.decl), + inv.args.map(dispatch), + inv.outArgs.map(dispatch), + inv.typeArgs.map(dispatch), + inv.givenMap.map { case (v, e) => (succ(v.decl), dispatch(e)) }, + inv.yields.map { case (e, v) => (dispatch(e), succ(v.decl)) }, + )(InstanceInvocationFailureToInvocationFailure(inv))(inv.o) + case inv: FunctionInvocation[Pre] => + implicit val o = inv.o + InstanceFunctionInvocation[Post]( + getGlobals, + funcSucc.ref(inv.ref.decl), + inv.args.map(dispatch), + inv.typeArgs.map(dispatch), + inv.givenMap.map { case (v, e) => (succ(v.decl), dispatch(e)) }, + inv.yields.map { case (e, v) => (dispatch(e), succ(v.decl)) }, + )(InstanceInvocationFailureToInvocationFailure(inv))(inv.o) + case _ => expr.rewriteDefault() + } + + override def dispatch(program: Program[Pre]): Program[Post] = { + program.rewrite(declarations = { + globalDeclarations.collect { + createGlobalClass(program) + program.declarations.map(dispatch) + }._1 + }) + } + + override def dispatch(decl: Declaration[Pre]): Unit = + decl match { + // Functions and procedures are moved into the global statics class + case _: Function[Pre] | _: Procedure[Pre] => decl.drop() + case cls: ByReferenceClass[Pre] => + cls.rewrite(intrinsicLockInvariant = spec { + cls.intrinsicLockInvariant.rewriteDefault() + }).succeed(cls) + case _ => super.dispatch(decl) + } + + override def dispatch( + contract: ApplicableContract[Pre] + ): ApplicableContract[Post] = spec { contract.rewriteDefault() } + + override def dispatch(contract: LoopContract[Pre]): LoopContract[Post] = + spec { contract.rewriteDefault() } + + override def dispatch(stmt: Statement[Pre]): Statement[Post] = + stmt match { + case assert: Assert[Pre] => + assert.rewrite(res = spec { assert.res.rewriteDefault() }) + case assume: Assume[Pre] => + assume.rewrite(assn = spec { assume.assn.rewriteDefault() }) + case inhale: Inhale[Pre] => + inhale.rewrite(res = spec { inhale.res.rewriteDefault() }) + case exhale: Exhale[Pre] => + exhale.rewrite(res = spec { exhale.res.rewriteDefault() }) + // Par blocks? + case _ => stmt.rewriteDefault() + } + + def createGlobalClass(program: Program[Pre]): Unit = { + globals.fill( + new ByReferenceClass( + decls = + classDeclarations.collect { + globalsConstructor.fill( + constructor( + cls = globals.ref, + body = Some(Block[Post](Seq())(program.o)), + blame = PanicBlame("Trivial contract"), + contractBlame = PanicBlame("Trivial contract"), + )(program.o).declare() + ) + program.declarations.collect { + case p: Procedure[Pre] => dispatchProc(p) + case f: Function[Pre] => dispatchFunc(f) + } + }._1, + typeArgs = Seq(), + supports = Seq(), + intrinsicLockInvariant = tt, + )(program.o.where(name = "G$")).declare() + ) + + implicit val o = program.o + ghostGlobals.fill(withResult[Post, Function[Post]](result => + function( + blame = PanicBlame("Trivial contract"), + contractBlame = TrueSatisfiable, + ensures = (result !== Null()).accounted, + returnType = TByReferenceClass[Post](globals.ref, Seq()), + )(program.o.where(name = "g$")).declare() + )) + } + + def dispatchProc(proc: Procedure[Pre]): Unit = + procSucc(proc) = + new InstanceMethod( + returnType = dispatch(proc.returnType), + args = variables.dispatch(proc.args), + outArgs = variables.dispatch(proc.outArgs), + typeArgs = variables.dispatch(proc.typeArgs), + body = proc.body.map(dispatch), + contract = dispatch(proc.contract), + inline = proc.inline, + pure = proc.pure, + )(proc.blame)(proc.o).declare() + + def dispatchFunc(func: Function[Pre]): Unit = + funcSucc(func) = + new InstanceFunction( + returnType = dispatch(func.returnType), + args = variables.dispatch(func.args), + typeArgs = variables.dispatch(func.typeArgs), + body = func.body.map(dispatch), + contract = dispatch(func.contract), + inline = func.inline, + threadLocal = func.threadLocal, + )(func.blame)(func.o).declare() + +} diff --git a/src/rewrite/vct/rewrite/veymont/GenerateAndEncodeChannels.scala b/src/rewrite/vct/rewrite/veymont/generation/GenerateAndEncodeChannels.scala similarity index 79% rename from src/rewrite/vct/rewrite/veymont/GenerateAndEncodeChannels.scala rename to src/rewrite/vct/rewrite/veymont/generation/GenerateAndEncodeChannels.scala index aa558481be..3708ec05b2 100644 --- a/src/rewrite/vct/rewrite/veymont/GenerateAndEncodeChannels.scala +++ b/src/rewrite/vct/rewrite/veymont/generation/GenerateAndEncodeChannels.scala @@ -1,4 +1,4 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.generation import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack @@ -7,9 +7,9 @@ import vct.col.ast.{ Block, ByReferenceClass, ChorRun, - EndpointStatement, Choreography, Class, + Committed, Communicate, CommunicateStatement, Constructor, @@ -18,17 +18,20 @@ import vct.col.ast.{ Deref, Endpoint, EndpointName, + EndpointStatement, Eval, Expr, FieldLocation, + Held, InstanceField, InstanceMethod, - InstancePredicate, IterationContract, Local, + Loop, LoopContract, LoopInvariant, Message, + Perm, Program, Receiver, Result, @@ -40,15 +43,16 @@ import vct.col.ast.{ TVar, ThisObject, Type, - Value, Variable, + WritePerm, } -import vct.col.origin.{Name, Origin, PanicBlame, SourceName} +import vct.col.origin._ import vct.col.ref.Ref import vct.col.rewrite.adt.ImportADTImporter import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg} -import vct.col.util.AstBuildHelpers._ +import vct.col.util.AstBuildHelpers.{value, _} import vct.col.util.SuccessionMap +import vct.rewrite.veymont.VeymontContext import scala.collection.mutable import scala.reflect.ClassTag @@ -118,6 +122,7 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( val currentCommunicate = ScopedStack[Communicate[Pre]]() val currentMsgTVar = ScopedStack[Variable[Pre]]() val currentMsgExpr = ScopedStack[Expr[Post]]() + val currentWriteRead = ScopedStack[InstanceMethod[Pre]]() val fieldOfCommunicate = SuccessionMap[(Endpoint[Pre], Communicate[Pre]), InstanceField[Post]]() @@ -184,9 +189,14 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( fieldOfCommunicate.ref((endpoint, comm)), )(PanicBlame("Shouldn't happen")) + def channelLockInv(comm: Communicate[Pre])(implicit o: Origin): Expr[Post] = + valueSender(comm) &* valueReceiver(comm) &* + dispatch(genericChannelClass.intrinsicLockInvariant) &* + thisHasMsg(comm) ==> dispatch(comm.invariant) + override def dispatch(p: Program[Pre]): Program[Post] = { mappings.program = p - p.rewriteDefault() + super.dispatch(p) } override def dispatch(decl: Declaration[Pre]): Unit = @@ -250,6 +260,8 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( } case cls: ByReferenceClass[Pre] if isEndpointClass(cls) => + // For each communicate in a choreography, add fields for the communicate channel to classes + // of endpoints participating in the choreography cls.rewrite(decls = classDeclarations.collect { cls.decls.foreach(dispatch) @@ -264,6 +276,30 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( }._1 ).succeed(cls) + case cons: Constructor[Pre] if classOfOpt(cons).exists(isEndpointClass) => + // For each communicate in the choreography, a field is added to the endpoint class + // Hence, we add full write permission for each of those fields in the postcondition + val cls = classOf(cons) + implicit val o = cons.o + val `this` = ThisObject[Post](succ(cls)) + val perms = foldStar(communicatesOf(choreographyOf(cls)).map { comm => + val ref: Ref[Post, InstanceField[Post]] = fieldOfCommunicate + .ref((endpointOf(cls), comm)) + Perm(FieldLocation[Post](`this`, ref), WritePerm()) + }) + cons.rewrite( + contract = cons.contract.rewrite(ensures = + perms.accounted &* dispatch(cons.contract.ensures) + ), + // Because we prepend an accounted predicate to the contract, split the blame left + blame = PostBlameSplit.left( + PanicBlame( + "Permissions for automatically generated fields should be managed correctly" + ), + cons.blame, + ), + ).succeed(cons) + case cls: ByReferenceClass[Pre] if cls == genericChannelClass => implicit val comm = currentCommunicate.top implicit val o = comm.o @@ -283,10 +319,7 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( )(o.where(name = "receiver")).declare() cls.decls.foreach(dispatch) }._1, - intrinsicLockInvariant = - valueSender &* valueReceiver &* - dispatch(cls.intrinsicLockInvariant) &* - thisHasMsg ==> dispatch(comm.invariant), + intrinsicLockInvariant = channelLockInv(comm), ).succeed(cls) } } @@ -313,6 +346,7 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( Assign(thisReceiver, receiver.get)(PanicBlame("Should be safe")), ) :+ cons.body.map(dispatch).getOrElse(skip) )), + // TODO (RR): Blame accounting is wrong here contract = cons.contract.rewrite(ensures = (valueSender &* valueReceiver &* (sender.get === thisSender) &* (receiver.get === thisReceiver)).accounted &* @@ -323,29 +357,33 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( case m: InstanceMethod[Pre] if m == genericChannelWrite => implicit val comm = currentCommunicate.top implicit val o = comm.o - currentMsgExpr.having(Local(succ(m.args.head))) { - channelWriteSucc(currentCommunicate.top) = m.rewrite(contract = - m.contract.rewrite(requires = - (valueSender &* valueReceiver &* dispatch(comm.invariant)) - .accounted &* dispatch(m.contract.requires) - ) - ).succeed(m) - } + channelWriteSucc(currentCommunicate.top) = m.rewrite( + contract = + currentMsgExpr.having(Local(succ(m.args.head))) { + m.contract.rewrite(requires = + (valueSender &* valueReceiver &* dispatch(comm.invariant)) + .accounted &* dispatch(m.contract.requires) + ) + }, + body = currentWriteRead.having(m) { m.body.map(dispatch) }, + ).succeed(m) case m: InstanceMethod[Pre] if m == genericChannelRead => implicit val comm = currentCommunicate.top implicit val o = comm.o - currentMsgExpr.having(Result(succ(m))) { - channelReadSucc(currentCommunicate.top) = m.rewrite[Post](contract = - m.contract.rewrite( - requires = (valueSender &* valueReceiver).accounted &* - dispatch(m.contract.requires), - ensures = - (valueSender &* valueReceiver &* dispatch(comm.invariant)) - .accounted &* dispatch(m.contract.requires), - ) - ).succeed(m) - } + channelReadSucc(currentCommunicate.top) = m.rewrite[Post]( + contract = + currentMsgExpr.having(Result(succ(m))) { + m.contract.rewrite( + requires = (valueSender &* valueReceiver).accounted &* + dispatch(m.contract.requires), + ensures = + (valueSender &* valueReceiver &* dispatch(comm.invariant)) + .accounted &* dispatch(m.contract.requires), + ) + }, + body = currentWriteRead.having(m) { m.body.map(dispatch) }, + ).succeed(m) case f: InstanceField[Pre] if f == genericChannelHasMsg => channelHasMsgSucc(currentCommunicate.top) = f.rewriteDefault() @@ -361,7 +399,7 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( if (currentCommunicate.nonEmpty) { rewriteChannelExpr(currentCommunicate.top, expr) } else - super.dispatch(expr) + expr.rewriteDefault() def rewriteChannelExpr( comm: Communicate[Pre], @@ -381,11 +419,17 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( } } + // For each communicate statement, there is a channel C. For each C, we generate the permissions for all the extra + // fields (sender, receiver), for each endpoint E, such that the fields are accessible to all endpoints. + // We also ensure it is invariant that the channels are committed. Finally, we generate annotations to indicate that + // the values in the sender/receiver fields are equal to actual intended endpoint. def channelContext(chor: Choreography[Pre])(implicit o: Origin): Expr[Post] = foldStar(chor.endpoints.flatMap { endpoint => communicatesOf(endpoint).map { comm => endpointComm(endpoint, comm).value &* getSender(endpoint, comm).value &* - getReceiver(endpoint, comm).value &* + getReceiver(endpoint, comm).value &* Committed( + endpointComm(endpoint, comm) + )(PanicBlame("Guaranteed not to be null")) &* (getSender(endpoint, comm) === EndpointName(succ(comm.sender.get.decl))) &* (getReceiver(endpoint, comm) === @@ -411,6 +455,18 @@ case class GenerateAndEncodeChannels[Pre <: Generation]( iter.rewrite(requires = (channelContext(chor)(chor.o) &* dispatch(iter.requires))(chor.o) ) + case inv: LoopInvariant[Pre] + if currentCommunicate.nonEmpty && currentWriteRead.nonEmpty => + implicit val comm = currentCommunicate.top + implicit val o = inv.o + inv.rewrite(invariant = Held(channelThis) &* channelLockInv(comm)) + case inv: IterationContract[Pre] => + implicit val comm = currentCommunicate.top + implicit val o = inv.o + inv.rewrite( + requires = Held(channelThis) &* channelLockInv(comm), + ensures = Held(channelThis) &* channelLockInv(comm), + ) case _ => contract.rewriteDefault() } diff --git a/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala b/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala new file mode 100644 index 0000000000..b044431b1f --- /dev/null +++ b/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala @@ -0,0 +1,430 @@ +package vct.rewrite.veymont.generation + +import com.typesafe.scalalogging.LazyLogging +import hre.util.ScopedStack +import vct.col.ast.{ + And, + TVoid, + ApplicableContract, + Assert, + Assign, + Assume, + Block, + Branch, + ByReferenceClass, + ChorPerm, + ChorRun, + ChorStatement, + Choreography, + Class, + ClassDeclaration, + Constructor, + Declaration, + Deref, + Endpoint, + EndpointExpr, + EndpointName, + EndpointStatement, + Eval, + Exhale, + Expr, + FieldLocation, + Fork, + IdleToken, + Inhale, + InstanceField, + InstanceMethod, + IterationContract, + Join, + Local, + Location, + Loop, + LoopContract, + LoopInvariant, + Node, + Or, + Perm, + Procedure, + Program, + RunMethod, + Scope, + Statement, + ThisObject, + Type, + Value, + Variable, + WritePerm, +} +import vct.col.origin.{Name, Origin, PanicBlame, PostBlameSplit} +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ +import vct.col.util.SuccessionMap +import vct.result.Message +import vct.result.VerificationError.SystemError +import vct.rewrite.veymont.VeymontContext +import vct.rewrite.veymont.generation.GenerateImplementation.CannotProjectStatement + +import scala.collection.mutable + +object GenerateImplementation extends RewriterBuilder { + override def key: String = "generateImplementation" + + override def desc: String = + "Generate classes for VeyMont threads in parallel program" + + case class CannotProjectStatement(endpoint: Endpoint[_], s: Statement[_]) + extends SystemError { + override def text: String = { + Message.messagesInContext( + ( + s.o, + s"The following statement was not transformed into a supported statement...", + ), + (endpoint.o, "... while projecting for this endpoint."), + ) + } + } +} + +case class GenerateImplementation[Pre <: Generation]() + extends Rewriter[Pre] with VeymontContext[Pre] with LazyLogging { + outer => + + val runSucc: mutable.LinkedHashMap[Choreography[Pre], Procedure[Post]] = + mutable.LinkedHashMap() + private val givenClassSucc: SuccessionMap[Type[Pre], Class[Post]] = + SuccessionMap() + private val givenClassConstrSucc: SuccessionMap[Type[Pre], Procedure[Pre]] = + SuccessionMap() + val endpointLocals: SuccessionMap[Endpoint[Pre], Variable[Post]] = + SuccessionMap() + + // For each endpoint and input variable, there is a unique instance field (on the class of the endpoint) + val endpointParamFields = + SuccessionMap[(Endpoint[Pre], Variable[Pre]), InstanceField[Post]]() + // For each endpoint and another endpoint, there is a unique instance field (on the class of the endpoint) + // with a reference to the second endpoint + val endpointPeerFields = + SuccessionMap[(Endpoint[Pre], Endpoint[Pre]), InstanceField[Post]]() + + val currentThis = ScopedStack[ThisObject[Post]]() + + override def dispatch(p: Program[Pre]): Program[Post] = { + mappings.program = p + super.dispatch(p) + } + + override def dispatch(decl: Declaration[Pre]): Unit = { + decl match { + case p: Procedure[Pre] => super.dispatch(p) + case cls: ByReferenceClass[Pre] if isEndpointClass(cls) => + val chor = choreographyOf(cls) + val endpoint = endpointOf(cls) + currentThis.having(ThisObject[Post](succ(cls))(cls.o)) { + cls.rewrite(decls = + classDeclarations.collect { + cls.decls.foreach(dispatch) + generateRunMethod(chor, endpointOf(cls)) + generateParamFields(chor, endpoint) + generatePeerFields(chor, endpoint) + }._1 + ).succeed(cls) + } + + case cons: Constructor[Pre] if isEndpointClass(classOf(cons)) => + implicit val o = cons.o + cons.rewrite( + contract = cons.contract.rewrite(ensures = + (IdleToken[Post](ThisObject(succ(classOf(cons)))) &* + endpointContext(endpointOf(classOf(cons)), perm = WritePerm())) + .accounted &* dispatch(cons.contract.ensures) + ), + blame = PostBlameSplit + .left(PanicBlame("Automatically generated permissions"), cons.blame), + ).succeed(cons) + + case cls: Class[Pre] => super.dispatch(cls) + case chor: Choreography[Pre] => + currentChoreography.having(chor) { + chor.drop() + chor.endpoints.foreach(_.drop()) + implicit val o = chor.o + + chor.endpoints.foreach(endpoint => + endpointLocals(endpoint) = + new Variable(dispatch(endpoint.t))(endpoint.o) + ) + + val initEndpoints = chor.endpoints.map { endpoint => + assignLocal[Post]( + endpointLocals(endpoint).get, + dispatch(endpoint.init), + ) + } + + // Initialize the fields on each endpoint class, representing the parameters of the choreography, and other endpoints + val auxFieldAssigns = chor.endpoints.flatMap { endpoint => + chor.params.map { param => + assignField[Post]( + endpointLocals(endpoint).get, + endpointParamFields.ref((endpoint, param)), + Local(succ(param)), + blame = PanicBlame("Should be safe"), + ) + } ++ chor.endpoints.map { peer => + assignField[Post]( + endpointLocals(endpoint).get, + endpointPeerFields.ref((endpoint, peer)), + endpointLocals(peer).get, + blame = PanicBlame("Should be safe"), + ) + } + } + + val forkJoins = + chor.endpoints.map { endpoint => + Fork[Post](endpointLocals(endpoint).get)(PanicBlame("")) + } ++ chor.endpoints.map { endpoint => + Join[Post](endpointLocals(endpoint).get)(PanicBlame("")) + } + + val mainBody = Scope( + chor.endpoints.map(endpointLocals(_)), + Block( + initEndpoints ++ + Seq(chor.preRun.map(dispatch).getOrElse(Block(Seq()))) ++ + auxFieldAssigns ++ forkJoins + )(chor.o), + ) + + globalDeclarations.declare( + new Procedure( + contract = chor.contract.rewriteDefault(), + returnType = TVoid[Post](), + args = variables.dispatch(chor.params), + body = Some(mainBody), + outArgs = Seq(), + typeArgs = Seq(), + )(PanicBlame("TODO: Procedure"))(chor.o) + ) + } + case other => super.dispatch(other) + } + } + + def generateRunMethod( + chor: Choreography[Pre], + endpoint: Endpoint[Pre], + ): Unit = { + val run = chor.run + implicit val o = run.o + currentChoreography.having(chor) { + currentEndpoint.having(endpoint) { + classDeclarations.declare( + new RunMethod( + body = Some(projectStmt(run.body)(endpoint)), + contract = projectContract(run.contract)(endpoint), + )(PanicBlame("")) + ) + } + } + } + + def generateParamFields( + chor: Choreography[Pre], + endpoint: Endpoint[Pre], + ): Unit = + chor.params.foreach { param => + val f = + new InstanceField(dispatch(param.t), Seq())(param.o.where(indirect = + Name.names( + chor.o.getPreferredNameOrElse(), + Name("p"), + param.o.getPreferredNameOrElse(), + ) + )) + classDeclarations.declare(f) + endpointParamFields((endpoint, param)) = f + } + + def generatePeerFields( + chor: Choreography[Pre], + endpoint: Endpoint[Pre], + ): Unit = + chor.endpoints.foreach { peer => + val f = + new InstanceField(dispatch(peer.t), Seq())( + endpoint.o + .where(indirect = Name.names(peer.o.getPreferredNameOrElse())) + ) + classDeclarations.declare(f) + endpointPeerFields((endpoint, peer)) = f + } + + // All permissions that we want to be in scope within the run method of an endpoint: + // the peer fields and param fields + def endpointContext( + endpoint: Endpoint[Pre], + perm: Expr[Post] = null, + value: Boolean = false, + )(implicit o: Origin): Expr[Post] = { + assert(value ^ (perm != null)) + + def makePerm(loc: Location[Post]): Expr[Post] = + if (perm != null) + Perm(loc, perm) + else + Value(loc) + + val cls = endpoint.cls.decl + val `this` = ThisObject[Post](succ(cls)) + val chor = choreographyOf(endpoint) + val peerPerms = foldStar(chor.endpoints.map { peer => + val ref = endpointPeerFields + .ref[Post, InstanceField[Post]]((endpoint, peer)) + makePerm(FieldLocation(`this`, ref)) + }) + + val paramPerms = foldStar(chor.params.map { param => + val ref = endpointParamFields + .ref[Post, InstanceField[Post]]((endpoint, param)) + makePerm(FieldLocation(`this`, ref)) + }) + + peerPerms &* paramPerms + } + + override def dispatch(statement: Statement[Pre]): Statement[Post] = { + if (currentEndpoint.nonEmpty) + projectStmt(statement)(currentEndpoint.top) + else + super.dispatch(statement) + } + + override def dispatch(expr: Expr[Pre]): Expr[Post] = + expr match { + case InChor(_, EndpointName(Ref(endpoint))) => + Local[Post](endpointLocals.ref(endpoint))(expr.o) + case InEndpoint(_, endpoint, EndpointName(Ref(peer))) => + implicit val o = expr.o + Deref[Post](currentThis.top, endpointPeerFields.ref((endpoint, peer)))( + PanicBlame("Shouldn't happen") + ) + case InEndpoint(_, endpoint, Local(Ref(v))) + if currentChoreography.nonEmpty && currentEndpoint.nonEmpty && + isChoreographyParam(v) => + implicit val o = expr.o + Deref[Post](currentThis.top, endpointParamFields.ref((endpoint, v)))( + PanicBlame("Shouldn't happen") + ) + case InEndpoint(_, endpoint, expr) => projectExpr(expr)(endpoint) + case _ => expr.rewriteDefault() + } + + def projectStmt( + statement: Statement[Pre] + )(implicit endpoint: Endpoint[Pre]): Statement[Post] = + statement match { + case EndpointStatement(None, statement) => + statement match { + case _ => + throw new Exception( + "Encountered ChorStatement without endpoint context" + ) + } + case EndpointStatement(Some(Ref(other)), inner) if other == endpoint => + inner match { + case assign: Assign[Pre] => assign.rewriteDefault() + case eval: Eval[Pre] => eval.rewriteDefault() + } + // Ignore statements that do not match the current endpoint + case EndpointStatement(_, _) => Block(Seq())(statement.o) + // Specialize composite statements to the current endpoint + case c @ ChorStatement(branch: Branch[Pre]) + if c.explicitEndpoints.contains(endpoint) => + implicit val o = branch.o + Branch[Post]( + Seq((projectExpr(branch.cond), projectStmt(branch.yes))) ++ + branch.no.map(no => Seq((tt[Post], projectStmt(no)))) + .getOrElse(Seq()) + ) + case c @ ChorStatement(l: Loop[Pre]) + if c.explicitEndpoints.contains(endpoint) => + implicit val o = l.o + loop( + cond = projectExpr(l.cond), + body = projectStmt(l.body), + contract = projectContract(l.contract), + ) + // Ignore loops, branches that the current endpoint doesn't participate in + case c @ ChorStatement(_: Loop[Pre] | _: Branch[Pre]) => Block(Seq())(c.o) + // Project assert-like statements as you'd expect + case ChorStatement(assert: Assert[Pre]) => + assert.rewrite(res = projectExpr(assert.res)) + case ChorStatement(assume: Assume[Pre]) => + assume.rewrite(assn = projectExpr(assume.assn)) + case ChorStatement(inhale: Inhale[Pre]) => + inhale.rewrite(res = projectExpr(inhale.res)) + case ChorStatement(exhale: Exhale[Pre]) => + exhale.rewrite(res = projectExpr(exhale.res)) + // Rewrite blocks transparently + case block: Block[Pre] => block.rewriteDefault() + // Don't let any missed cases slip through + case s => throw CannotProjectStatement(endpoint, s) + } + + def projectContract( + contract: LoopContract[Pre] + )(implicit endpoint: Endpoint[Pre]): LoopContract[Post] = { + implicit val o = contract.o + contract match { + case inv: LoopInvariant[Pre] => + inv.rewrite(invariant = + endpointContext(endpoint, value = true) &* projectExpr(inv.invariant) + ) + case it: IterationContract[Pre] => + it.rewrite( + requires = + endpointContext(endpoint, value = true) &* projectExpr(it.requires), + ensures = + endpointContext(endpoint, value = true) &* projectExpr(it.ensures), + ) + } + } + + def projectContract( + contract: ApplicableContract[Pre] + )(implicit endpoint: Endpoint[Pre]): ApplicableContract[Post] = { + implicit val o = contract.o + contract.rewrite( + requires = + endpointContext(endpoint, value = true).accounted &* + mapPredicate(contract.requires, projectExpr), + ensures = + endpointContext(endpoint, value = true).accounted &* + mapPredicate(contract.ensures, projectExpr), + contextEverywhere = projectExpr(contract.contextEverywhere), + ) + } + + def projectExpr( + expr: Expr[Pre] + )(implicit endpoint: Endpoint[Pre]): Expr[Post] = + expr match { + case ChorPerm(Ref(other), loc, perm) if endpoint == other => + Perm(dispatch(loc), dispatch(perm))(expr.o) + case ChorPerm(Ref(other), _, _) if endpoint != other => tt + case EndpointExpr(Ref(other), expr) if endpoint == other => + projectExpr(expr) + case EndpointExpr(_, _) => tt + // Define transparent projections for basic operators + case and: And[Pre] => + and.rewrite(projectExpr(and.left), projectExpr(and.right)) + case or: Or[Pre] => + or.rewrite(projectExpr(or.left), projectExpr(or.right)) + // Actually this is kind of wrong and buggy. But it covers most default & correct cases so + // I'll leave it for now + case _ => expr.rewriteDefault() + } +} diff --git a/src/rewrite/vct/rewrite/veymont/generation/ImplicationToTernary.scala b/src/rewrite/vct/rewrite/veymont/generation/ImplicationToTernary.scala new file mode 100644 index 0000000000..cf76ace5aa --- /dev/null +++ b/src/rewrite/vct/rewrite/veymont/generation/ImplicationToTernary.scala @@ -0,0 +1,18 @@ +package vct.rewrite.veymont.generation + +import vct.col.ast.{Expr, Implies, Select} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ + +object ImplicationToTernary extends RewriterBuilder { + override def key: String = "implicationToTernary" + override def desc: String = "Rewrites `p ==> q` to `p ? q : true`." +} + +case class ImplicationToTernary[Pre <: Generation]() extends Rewriter[Pre] { + override def dispatch(expr: Expr[Pre]): Expr[Post] = + expr match { + case Implies(p, q) => Select(dispatch(p), dispatch(q), tt)(expr.o) + case _ => expr.rewriteDefault() + } +} diff --git a/src/rewrite/vct/rewrite/veymont/SpecializeEndpointClasses.scala b/src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala similarity index 52% rename from src/rewrite/vct/rewrite/veymont/SpecializeEndpointClasses.scala rename to src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala index f07c731c2a..eef433d8ea 100644 --- a/src/rewrite/vct/rewrite/veymont/SpecializeEndpointClasses.scala +++ b/src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala @@ -2,26 +2,38 @@ package vct.rewrite.veymont import com.typesafe.scalalogging.LazyLogging import vct.col.ast.{ + ChorRun, ByReferenceClass, Choreography, Class, + Communicate, Constructor, Declaration, Deref, Endpoint, + EndpointExpr, EndpointName, Expr, + FieldLocation, InstanceField, + IterationContract, + LoopContract, + LoopInvariant, + Program, + Receiver, + Sender, ThisObject, UnitAccountedPredicate, + Value, Variable, WritePerm, } -import vct.col.origin.{Name, PanicBlame} +import vct.col.origin.{Name, Origin, PanicBlame, PostBlameSplit} import vct.col.ref.Ref import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.util.AstBuildHelpers._ import vct.col.util.SuccessionMap +import vct.rewrite.veymont.VeymontContext object SpecializeEndpointClasses extends RewriterBuilder { override def key: String = "specializeEndpointClasses" @@ -32,16 +44,30 @@ object SpecializeEndpointClasses extends RewriterBuilder { case class SpecializeEndpointClasses[Pre <: Generation]() extends Rewriter[Pre] with LazyLogging with VeymontContext[Pre] { - val implFieldOfEndpoint = SuccessionMap[Endpoint[Pre], InstanceField[Post]]() + val implFields = SuccessionMap[Endpoint[Pre], InstanceField[Post]]() val classOfEndpoint = SuccessionMap[Endpoint[Pre], Class[Post]]() + override def dispatch(p: Program[Pre]): Program[Post] = { + mappings.program = p + super.dispatch(p) + } + + def readImplField(obj: Expr[Post], endpoint: Endpoint[Pre])( + implicit o: Origin + ): Expr[Post] = { + Deref[Post](obj, implFields.ref(endpoint))(PanicBlame( + "Permissions for impl should be automatically generated" + )) + } + override def dispatch(expr: Expr[Pre]): Expr[Post] = expr match { - case name @ EndpointName(Ref(endpoint)) => - implicit val o = name.o - Deref[Post](name.rewriteDefault(), implFieldOfEndpoint.ref(endpoint))( - PanicBlame("Should be safe") - ) + case EndpointName(Ref(endpoint)) => + readImplField(expr.rewriteDefault(), endpoint)(expr.o) + case Sender(Ref(comm)) => + readImplField(expr.rewriteDefault(), comm.sender.get.decl)(expr.o) + case Receiver(Ref(comm)) => + readImplField(expr.rewriteDefault(), comm.receiver.get.decl)(expr.o) case _ => expr.rewriteDefault() } @@ -57,7 +83,7 @@ case class SpecializeEndpointClasses[Pre <: Generation]() new InstanceField[Post](dispatch(endpoint.t), Seq())( o.where(name = "impl") ) - implFieldOfEndpoint(endpoint) = implField + implFields(endpoint) = implField val constructor: Constructor[Post] = { val implArg = new Variable(dispatch(endpoint.t)) @@ -109,6 +135,66 @@ case class SpecializeEndpointClasses[Pre <: Generation]() ), ), ) + + case comm: Communicate[Pre] => + val sender = comm.sender.get.decl + val receiver = comm.receiver.get.decl + val newComm: Ref[Post, Communicate[Post]] = succ(comm) + implicit val o = comm.o + comm.rewrite(invariant = + value[Post](Sender(newComm), implFields.ref(sender)) &* + value[Post](Receiver(newComm), implFields.ref(receiver)) &* + dispatch(comm.invariant) + ).succeed(comm) + case _ => super.dispatch(decl) } + + override def dispatch(run: ChorRun[Pre]): ChorRun[Post] = { + implicit val o = run.o + run.rewrite( + contract = run.contract.rewrite( + requires = + specializeContext(currentChoreography.top).accounted &* + dispatch(run.contract.requires), + ensures = + specializeContext(currentChoreography.top).accounted &* + dispatch(run.contract.ensures), + ), + blame = PostBlameSplit + .left(PanicBlame("Automatically generated permissions"), run.blame), + ) + } + + override def dispatch(contract: LoopContract[Pre]): LoopContract[Post] = + contract match { + case InChor(chor, inv: LoopInvariant[Pre]) => + implicit val o = contract.o + inv.rewrite(invariant = + specializeContext(chor) &* dispatch(inv.invariant) + ) + case InChor(chor, inv: IterationContract[Pre]) => + implicit val o = contract.o + inv.rewrite( + requires = specializeContext(chor) &* dispatch(inv.requires), + ensures = specializeContext(chor) &* dispatch(inv.ensures), + ) + case _ => contract.rewriteDefault() + } + + // Within a choreography, we need to propagate permission for the impl fields of all endpoint to all endpoints + def specializeContext( + chor: Choreography[Pre] + )(implicit o: Origin): Expr[Post] = { + foldStar(chor.endpoints.flatMap { endpoint => + chor.endpoints.map { peer => + EndpointExpr[Post]( + succ(endpoint), + Value( + FieldLocation(EndpointName[Post](succ(peer)), implFields.ref(peer)) + ), + ) + } + }) + } } diff --git a/src/rewrite/vct/rewrite/veymont/EncodeChannels.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChannels.scala similarity index 81% rename from src/rewrite/vct/rewrite/veymont/EncodeChannels.scala rename to src/rewrite/vct/rewrite/veymont/verification/EncodeChannels.scala index 53f42119cc..10a1f480ea 100644 --- a/src/rewrite/vct/rewrite/veymont/EncodeChannels.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodeChannels.scala @@ -1,87 +1,18 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.verification import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack -import vct.col.ast.{ - Assert, - Assign, - Block, - ByValueClass, - ChorStatement, - BooleanValue, - ChorExpr, - ChorPerm, - ChorRun, - Choreography, - Class, - Communicate, - CommunicateStatement, - Constructor, - ConstructorInvocation, - Declaration, - Deref, - Endpoint, - EndpointExpr, - EndpointName, - EndpointStatement, - Eval, - Exhale, - Expr, - FieldLocation, - Inhale, - InstanceField, - InstanceMethod, - InstancePredicate, - IterationContract, - Local, - LoopContract, - LoopInvariant, - Message, - Perm, - Program, - Receiver, - Result, - Scope, - Sender, - Statement, - TByValueClass, - TClass, - TVar, - ThisObject, - Type, - Value, - Variable, -} -import vct.col.origin.{ - AssertFailed, - AssignLocalOk, - Blame, - ChannelInvariantNotEstablished, - ChannelInvariantNotEstablishedLocally, - ExhaleFailed, - Name, - Origin, - PanicBlame, - SourceName, -} +import vct.col.ast._ +import vct.col.origin._ import vct.col.ref.{DirectRef, Ref} -import vct.col.rewrite.adt.ImportADTImporter -import vct.col.rewrite.{ - Generation, - Rewriter, - RewriterBuilder, - RewriterBuilderArg, -} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.util.AstBuildHelpers._ import vct.col.util.SuccessionMap -import vct.rewrite.veymont.EncodeChannels.{ +import vct.rewrite.veymont.VeymontContext +import vct.rewrite.veymont.verification.EncodeChannels.{ AssertFailedToChannelInvariantNotEstablished, ExhaleFailedToChannelInvariantNotEstablished, } -import vct.rewrite.veymont.EncodeChoreography.AssertFailedToParticipantsNotDistinct - -import scala.collection.mutable -import scala.reflect.ClassTag object EncodeChannels extends RewriterBuilder { override def key: String = "encodeChannels" @@ -109,6 +40,11 @@ case class EncodeChannels[Pre <: Generation]() val includeChorExpr = ScopedStack[Boolean]() val substitutions = ScopedStack[Map[Expr[Pre], Expr[Post]]]() + override def dispatch(p: Program[Pre]): Program[Post] = { + mappings.program = p + super.dispatch(p) + } + override def dispatch(decl: Declaration[Pre]): Unit = decl match { case chor: Choreography[Pre] => diff --git a/src/rewrite/vct/rewrite/veymont/EncodeChorBranchUnanimity.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala similarity index 94% rename from src/rewrite/vct/rewrite/veymont/EncodeChorBranchUnanimity.scala rename to src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala index 01c8a70d75..0b005de1eb 100644 --- a/src/rewrite/vct/rewrite/veymont/EncodeChorBranchUnanimity.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala @@ -1,18 +1,12 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.verification import hre.util.ScopedStack import vct.col.ast._ -import vct.col.origin.{ - AssertFailed, - Blame, - BranchUnanimityFailed, - LoopUnanimityNotEstablished, - LoopUnanimityNotMaintained, - Origin, -} +import vct.col.origin._ import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg} import vct.col.util.AstBuildHelpers._ -import vct.rewrite.veymont.EncodeChorBranchUnanimity.{ +import vct.rewrite.veymont.VeymontContext +import vct.rewrite.veymont.verification.EncodeChorBranchUnanimity.{ ForwardBranchUnanimity, ForwardLoopUnanimityNotEstablished, ForwardLoopUnanimityNotMaintained, @@ -62,9 +56,10 @@ case class EncodeChorBranchUnanimity[Pre <: Generation](enabled: Boolean) val currentLoop = ScopedStack[Loop[Pre]]() override def dispatch(program: Program[Pre]): Program[Post] = - if (enabled) + if (enabled) { + mappings.program = program super.dispatch(program) - else + } else IdentityRewriter().dispatch(program) override def dispatch(decl: Declaration[Pre]): Unit = diff --git a/src/rewrite/vct/rewrite/veymont/EncodeChoreography.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChoreography.scala similarity index 96% rename from src/rewrite/vct/rewrite/veymont/EncodeChoreography.scala rename to src/rewrite/vct/rewrite/veymont/verification/EncodeChoreography.scala index 2c3ef88999..f22ed7dd10 100644 --- a/src/rewrite/vct/rewrite/veymont/EncodeChoreography.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodeChoreography.scala @@ -1,4 +1,4 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.verification import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack @@ -36,30 +36,12 @@ import vct.col.ast.{ Value, Variable, } -import vct.col.origin.{ - AssertFailed, - AssignFailed, - AssignLocalOk, - Blame, - CallableFailure, - ChorRunContextEverywhereFailedInPre, - ChorRunPreconditionFailed, - ContextEverywhereFailedInPre, - ContractedFailure, - ExceptionNotInSignals, - InvocationFailure, - Origin, - PanicBlame, - ParticipantsNotDistinct, - PreconditionFailed, - SeqAssignInsufficientPermission, - SignalsFailed, -} +import vct.col.origin._ +import vct.col.ref.Ref import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.util.AstBuildHelpers._ import vct.col.util.SuccessionMap import vct.result.VerificationError.Unreachable -import vct.col.ref.Ref import scala.collection.{mutable => mut} diff --git a/src/rewrite/vct/rewrite/veymont/EncodeEndpointInequalities.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeEndpointInequalities.scala similarity index 83% rename from src/rewrite/vct/rewrite/veymont/EncodeEndpointInequalities.scala rename to src/rewrite/vct/rewrite/veymont/verification/EncodeEndpointInequalities.scala index e1ed3e8b7a..b3e736b41f 100644 --- a/src/rewrite/vct/rewrite/veymont/EncodeEndpointInequalities.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodeEndpointInequalities.scala @@ -1,48 +1,11 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.verification import com.typesafe.scalalogging.LazyLogging -import hre.util.ScopedStack -import vct.col.ast.{ - ApplicableContract, - Assert, - Assume, - Block, - Choreography, - CommunicateStatement, - Declaration, - Endpoint, - EndpointName, - Expr, - IterationContract, - LoopContract, - LoopInvariant, - Neq, - Null, - Program, - SplitAccountedPredicate, - Statement, - UnitAccountedPredicate, -} -import vct.col.origin.{ - AssertFailed, - Blame, - BranchUnanimityFailed, - LoopUnanimityNotEstablished, - LoopUnanimityNotMaintained, - Origin, -} +import vct.col.ast._ 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.EncodeChorBranchUnanimity.{ - ForwardBranchUnanimity, - ForwardLoopUnanimityNotEstablished, - ForwardLoopUnanimityNotMaintained, -} -import vct.col.util.AstBuildHelpers._ -import vct.result.VerificationError -import vct.rewrite.veymont.EncodeChoreography.AssertFailedToParticipantsNotDistinct +import vct.rewrite.veymont.VeymontContext +import vct.rewrite.veymont.verification.EncodeChoreography.AssertFailedToParticipantsNotDistinct import scala.collection.mutable @@ -84,6 +47,11 @@ case class EncodeEndpointInequalities[Pre <: Generation]() ) } + override def dispatch(p: Program[Pre]): Program[Post] = { + mappings.program = p + super.dispatch(p) + } + override def dispatch(decl: Declaration[Pre]): Unit = decl match { case chor: Choreography[Pre] => diff --git a/src/rewrite/vct/rewrite/veymont/EncodePermissionStratification.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala similarity index 95% rename from src/rewrite/vct/rewrite/veymont/EncodePermissionStratification.scala rename to src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala index 557071f1e5..1248a58798 100644 --- a/src/rewrite/vct/rewrite/veymont/EncodePermissionStratification.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala @@ -1,40 +1,16 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.verification import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack import vct.col.ast._ -import vct.col.rewrite.{ - Generation, - Rewriter, - RewriterBuilder, - RewriterBuilderArg, -} +import vct.col.origin._ +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg} import vct.col.util.AstBuildHelpers._ import vct.col.util.SuccessionMap -import vct.result.VerificationError.{Unreachable, UserError} -import EncodeChoreography.{ - AssertFailedToParticipantsNotDistinct, - AssignFailedToSeqAssignFailure, -} -import vct.col.origin.{ - Blame, - ChorRunPreconditionFailed, - ExhaleFailed, - FoldFailed, - InsufficientPermission, - InvocationFailure, - Name, - Origin, - PanicBlame, - PreconditionFailed, - UnfoldFailed, - UnfoldFailure, - VerificationFailure, -} -import vct.col.ref.Ref -import vct.rewrite.veymont import vct.result.VerificationError.UserError -import vct.rewrite.veymont.EncodePermissionStratification.{ +import vct.rewrite.veymont.{InferEndpointContexts, VeymontContext} +import vct.rewrite.veymont.verification.EncodePermissionStratification.{ ForwardExhaleFailedToChorRun, ForwardInvocationFailureToDeref, ForwardUnfoldFailedToDeref, @@ -87,7 +63,7 @@ object EncodePermissionStratification extends RewriterBuilderArg[Boolean] { we implement an incomplete approach in EncodeChannels.scala. */ case class EncodePermissionStratification[Pre <: Generation]( - veymontGeneratePermissions: Boolean + generatePermissions: Boolean ) extends Rewriter[Pre] with VeymontContext[Pre] with LazyLogging { val inChor = ScopedStack[Boolean]() @@ -234,9 +210,9 @@ case class EncodePermissionStratification[Pre <: Generation]( } } - override def dispatch(program: Program[Pre]): Program[Post] = { - mappings.program = program - super.dispatch(program) + override def dispatch(p: Program[Pre]): Program[Post] = { + mappings.program = p + super.dispatch(p) } override def dispatch(decl: Declaration[Pre]): Unit = @@ -416,7 +392,7 @@ case class EncodePermissionStratification[Pre <: Generation]( blame = ForwardInvocationFailureToDeref(deref), ) - case ChorExpr(inner) if veymontGeneratePermissions => + case ChorExpr(inner) if generatePermissions => implicit val o = expr.o def predicates( @@ -468,7 +444,7 @@ case class EncodePermissionStratification[Pre <: Generation]( )) } - case ChorExpr(inner) if !veymontGeneratePermissions => + 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) } @@ -478,10 +454,10 @@ case class EncodePermissionStratification[Pre <: Generation]( // ... 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) && veymontGeneratePermissions => + if inChor.topOption.contains(true) && generatePermissions => inv.rewriteDefault() case inv: InstanceFunctionInvocation[Pre] - if inChor.topOption.contains(true) && veymontGeneratePermissions => + if inChor.topOption.contains(true) && generatePermissions => inv.rewriteDefault() case InEndpoint(_, endpoint, inv: FunctionInvocation[Pre]) => diff --git a/src/rewrite/vct/rewrite/veymont/PushInChor.scala b/src/rewrite/vct/rewrite/veymont/verification/PushInChor.scala similarity index 88% rename from src/rewrite/vct/rewrite/veymont/PushInChor.scala rename to src/rewrite/vct/rewrite/veymont/verification/PushInChor.scala index 1e7763e04c..1ec78e6159 100644 --- a/src/rewrite/vct/rewrite/veymont/PushInChor.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/PushInChor.scala @@ -1,17 +1,10 @@ -package vct.rewrite.veymont +package vct.rewrite.veymont.verification import hre.util.ScopedStack -import vct.col.ast.{ - AnyFunctionInvocation, - ChorExpr, - Communicate, - Declaration, - Expr, - Program, - Statement, -} +import vct.col.ast._ import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg} import vct.col.util.AstBuildHelpers._ +import vct.rewrite.veymont.InferEndpointContexts object PushInChor extends RewriterBuilderArg[Boolean] { override def key: String = "pushInChor" @@ -20,7 +13,7 @@ object PushInChor extends RewriterBuilderArg[Boolean] { "Pushes in `\\chor` expressions when generating permissions. This simplifies later analysis to be done by encodePermissionStratification." } -case class PushInChor[Pre <: Generation](veymontGeneratePermissions: Boolean) +case class PushInChor[Pre <: Generation](generatePermissions: Boolean) extends Rewriter[Pre] { case class IdentityRewriter[Pre <: Generation]() extends Rewriter[Pre] {} @@ -28,7 +21,7 @@ case class PushInChor[Pre <: Generation](veymontGeneratePermissions: Boolean) val inInvariant = ScopedStack[Boolean]() override def dispatch(program: Program[Pre]): Program[Post] = - if (veymontGeneratePermissions) + if (generatePermissions) program.rewriteDefault() else IdentityRewriter().dispatch(program) @@ -61,7 +54,7 @@ case class PushInChor[Pre <: Generation](veymontGeneratePermissions: Boolean) // expression in an EndpointExpr, which will in turn cause read functions to be used by EncodePermissionStratification // This doesn't make analysis more powerful, but it might save a chain of unfoldings here and there. // In addition, this optimization is only possible when generating permissions, as indicated by the - // veymontGeneratePermissions parameter, because only then we know the owner of each field, which is what makes + // generatePermissions parameter, because only then we know the owner of each field, which is what makes // wrapping exprs in EndpointExpr's safe: they explicitly model the semantics of permission generation. def needsChor(expr: Expr[Pre]): Boolean = containsFunctionInvocation(expr) || countEndpoints(expr) > 1 diff --git a/test/main/vct/test/integration/examples/PermutationSpec.scala b/test/main/vct/test/integration/examples/PermutationSpec.scala index 83130992ef..ec1e0c3ae5 100644 --- a/test/main/vct/test/integration/examples/PermutationSpec.scala +++ b/test/main/vct/test/integration/examples/PermutationSpec.scala @@ -4,7 +4,7 @@ import vct.test.integration.helper.VercorsSpec class PermutationSpec extends VercorsSpec { vercors should verify using silicon example "publications/2020/permutations/permutation.pvl" - vercors should verify using silicon examples("publications/2020/permutations/evenPhase.pvl", "publications/2020/permutations/permutation.pvl") + // vercors should verify using silicon examples("publications/2020/permutations/evenPhase.pvl", "publications/2020/permutations/permutation.pvl") vercors should verify using silicon examples("publications/2020/permutations/oddEven.pvl", "publications/2020/permutations/permutation.pvl") // vercors should verify using silicon examples("publications/2020/permutations/oddPhase.pvl", "publications/2020/permutations/permutation.pvl) vercors should verify using silicon examples("publications/2020/permutations/bubble.pvl", "publications/2020/permutations/permutation.pvl") diff --git a/test/main/vct/test/integration/examples/veymont/FM2023VeyMontSpec.scala b/test/main/vct/test/integration/examples/veymont/FM2023VeyMontSpec.scala index 849ab2bb4b..aa4b47e12f 100644 --- a/test/main/vct/test/integration/examples/veymont/FM2023VeyMontSpec.scala +++ b/test/main/vct/test/integration/examples/veymont/FM2023VeyMontSpec.scala @@ -1,26 +1,23 @@ package vct.test.integration.examples.veymont -import vct.test.integration.helper.VercorsSpec +import vct.test.integration.helper.VeyMontSpec -class FM2023VeyMontSpec extends VercorsSpec { +class FM2023VeyMontSpec extends VeyMontSpec { val wd = "publications/2023/FM2023VeyMont" val applicability = s"$wd/applicability" val paperExamples = s"$wd/paper-examples" + val fs = Seq("--generate-permissions") - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$applicability/2pc-3.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$applicability/2pc-5.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$applicability/consensus-3.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$applicability/consensus-5.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$applicability/election-3.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$applicability/election-5.pvl" + // Verify with generated permissions + choreography(inputs = examples(s"$applicability/2pc-3.pvl"), flags = fs) + choreography(inputs = examples(s"$applicability/2pc-5.pvl"), flags = fs) + choreography(inputs = examples(s"$applicability/consensus-3.pvl"), flags = fs) + choreography(inputs = examples(s"$applicability/consensus-5.pvl"), flags = fs) + choreography(inputs = examples(s"$applicability/election-3.pvl"), flags = fs) + choreography(inputs = examples(s"$applicability/election-5.pvl"), flags = fs) - vercors should verify using silicon example s"$paperExamples/veymont-swap.pvl" + // Verify without generated permissions + choreography(inputs = examples(s"$paperExamples/veymont-swap.pvl")) // Slow because of generated permisissions. Can fix when VeyMont has permission support. For now in known-problems // Also: needs sub runs, otherwise the program blows up quite a bit. diff --git a/test/main/vct/test/integration/examples/veymont/IFM2024VeyMontPermissionsSpec.scala b/test/main/vct/test/integration/examples/veymont/IFM2024VeyMontPermissionsSpec.scala new file mode 100644 index 0000000000..26e0a3bc5f --- /dev/null +++ b/test/main/vct/test/integration/examples/veymont/IFM2024VeyMontPermissionsSpec.scala @@ -0,0 +1,200 @@ +package vct.test.integration.examples.veymont + +import hre.util.{FilesHelper, Patch} +import vct.test.integration.helper.{VercorsSpec, VeyMontSpec} + +import java.io.{ + ByteArrayOutputStream, + File, + FileDescriptor, + FileOutputStream, + PrintStream, +} +import java.net.URLClassLoader +import java.nio.charset.StandardCharsets +import java.nio.file.{Files, Path, Paths} +import scala.sys.process.Process + +class IFM2024VeyMontPermissionsSpec extends VeyMontSpec { + val wd = Paths.get("publications/2024/IFM2024VeyMontPermissions") + + { + val caseWd = wd.resolve("0-TTT") + veymontTest( + desc = "TTT case study (choreographic verification)", + inputs = examplePaths( + caseWd.resolve("Move.pvl"), + caseWd.resolve("Player.pvl"), + caseWd.resolve("0-TTT.pvl"), + ), + flags = Seq( + "--generate-permissions", + // Skip implementation verification. This version of 0-TTT does not support that (time constraints). + "--veymont-skip-implementation-verification", + ), + ) + } + + { + val caseWd = wd.resolve("1-TTTmsg") + + veymontTest( + desc = "TTTmsg case study (choreograpy verification)", + inputs = examplePaths( + caseWd.resolve("Move.pvl"), + caseWd.resolve("Player.pvl"), + caseWd.resolve("1-TTTmsg.pvl"), + ), + flags = Seq( + "--dev-unsafe-optimization", + "--veymont-skip-implementation-verification", + ), + ) + + veymontTest( + desc = "TTTmsg case study (implementation verification)", + inputs = examplePaths( + caseWd.resolve("Move.pvl"), + caseWd.resolve("Player.pvl"), + caseWd.resolve("1-TTTmsg.pvl"), + ), + flags = Seq( + "--dev-unsafe-optimization", + "--veymont-skip-choreography-verification", + ), + ) + + veymontTest( + desc = "TTTmsg case study (implementation execution)", + inputs = examplePaths( + caseWd.resolve("Move.pvl"), + caseWd.resolve("Player.pvl"), + caseWd.resolve("1-TTTmsg.pvl"), + ), + flags = Seq( + "--dev-unsafe-optimization", + "--veymont-skip-choreography-verification", + "--veymont-skip-implementation-verification", + ), + targetLanguage = Java, + processImplementation = runTttImplementation, + ) + } + + { + val caseWd = wd.resolve("2-TTTlast") + + veymontTest( + desc = "TTTlast case study (choreography verification)", + inputs = examplePaths( + caseWd.resolve("Move.pvl"), + caseWd.resolve("Player.pvl"), + caseWd.resolve("2-TTTlast.pvl"), + ), + flags = Seq( + "--dev-unsafe-optimization", + "--veymont-skip-implementation-verification", + ), + ) + + veymontTest( + desc = "TTTlast case study (implementation verification)", + inputs = examplePaths( + caseWd.resolve("Move.pvl"), + caseWd.resolve("Player.pvl"), + caseWd.resolve("2-TTTlast.pvl"), + ), + flags = Seq( + "--dev-unsafe-optimization", + "--veymont-skip-choreography-verification", + ), + ) + + veymontTest( + desc = "TTTlast case study (implementation execution)", + inputs = examplePaths( + caseWd.resolve("Move.pvl"), + caseWd.resolve("Player.pvl"), + caseWd.resolve("2-TTTlast.pvl"), + ), + flags = Seq( + "--dev-unsafe-optimization", + "--veymont-skip-implementation-verification", + "--veymont-skip-choreography-verification", + ), + targetLanguage = Java, + processImplementation = runTttImplementation, + ) + } + + ///////////////////// + // Testing helpers // + ///////////////////// + + val patchFile = example(wd.resolve("testFiles/patches.txt")) + val scriptFile = example(wd.resolve("testFiles/testScript.txt")) + // Given a TTT implementation in java at path p, patches it to be fully executable + // by adding implementations and adding hooks such that it is possible to inspect the final + // state with external code, runs it, and asserts that + // the output expected is equal to each player just picking the first field + // location that is available. + def runTttImplementation(p: Path): Unit = { + val source = Files.readString(p) + val patches = Patch.fromFile(patchFile) + val patched = Patch.applyAll(patches, source) + val testScript = Files.readString(scriptFile) + val output = runJava(testScript, patched) + info("== Executed code output ==") + info(output) + assert(output == """p1: + |0 1 0 + |1 0 1 + |0 -1 -1 + |p2: + |0 1 0 + |1 0 1 + |0 -1 -1 + |""".stripMargin) + } + + /** Runs the given Java script and returns the captured standard output. + * Requires the JDK being present on the current system. + * + * @param script + * A series of java statements to be executed. May refer to declarations in + * the declarations parameter. + * @param declarations + * A series of non-public java declarations, no package declaration. + * Imports at the beginning are supported. + */ + def runJava(script: String, declarations: String): String = { + val cls = "MyScriptContainer" + val source = s"$declarations\n\npublic class $cls { static { $script } }" + + // Save source in .java file. + val root: Path = Files.createTempDirectory("java") + val sourceFile = root.resolve(s"$cls.java") + Files.createFile(sourceFile) + Files.write(sourceFile, source.getBytes(StandardCharsets.UTF_8)) + + // Compile source file. + info( + s"Invoking javac to compile generated code; expecting it to be available, otherwise this test will fail." + ) + Process(Seq("javac", sourceFile.toString), sourceFile.getParent.toFile).! + + // Capture stdout + val stdoutCapture = new ByteArrayOutputStream(); + System.setOut(new PrintStream(stdoutCapture)); + + // Load and instantiate compiled class. + val classLoader = URLClassLoader.newInstance(Array(root.toUri.toURL)) + Class.forName(cls, true, classLoader) + + // Reset system stdout + System.setOut(new PrintStream(new FileOutputStream(FileDescriptor.out))); + + // Return captured stdout + stdoutCapture.toString() + } +} diff --git a/test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala b/test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala index 22450733a1..78db322984 100644 --- a/test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala +++ b/test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala @@ -1,10 +1,25 @@ package vct.test.integration.examples.veymont -import vct.test.integration.helper.VercorsSpec +import vct.test.integration.helper.VeyMontSpec -class TechnicalVeyMontSpec extends VercorsSpec { - vercors should fail withCode "perm" using silicon in - "Bobby may receive permission for its target location" pvl """ +class TechnicalVeyMontSpec extends VeyMontSpec { + implementation( + desc = "Run contract can depend on choreography contract", + pvl = """ + class Storage {} + + requires x > 0; + choreography Chor(int x) { + endpoint alex = Storage(); + + requires x > 0; + run { } + }""", + ) + + choreography( + desc = "Bobby may receive permission for its target location", + pvl = """ class Storage { int x; int y; } choreography Chor() { endpoint alex = Storage(); @@ -14,11 +29,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { channel_invariant Perm(bobby.x, 1); communicate alex.x -> bobby.x; } - } - """ - - vercors should fail withCode "perm" using silicon in - "Bobby might not have permission to assign" pvl """ + }""", + fail = "perm", + ) + + choreography( + desc = "Bobby might not have permission to assign", + fail = "perm", + pvl = """ class Storage { int x; int y; } choreography Chor() { endpoint alex = Storage(); @@ -28,10 +46,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate alex.x -> bobby.x; } } - """ + """, + ) - vercors should fail withCode "channelInvariantNotEstablished:false" using - silicon in "Channel invariant might not be established" pvl """ + choreography( + desc = "Channel invariant might not be established", + fail = "channelInvariantNotEstablished:false", + pvl = """ class Storage { int x; int y; } choreography Chor() { endpoint alex = Storage(); @@ -42,10 +63,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate alex.x -> bobby.x; } } - """ + """, + ) - (vercors should verify using silicon flag "--veymont-generate-permissions" in - "example using communicate" pvl """ + choreography( + desc = "example using communicate", + flag = "--generate-permissions", + pvl = """ class Storage { int x; } @@ -61,11 +85,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate bob.x -> alice.x; } } - """) - - (vercors should fail withCode "assertFailed:false" using silicon flag - "--veymont-generate-permissions" in - "plain endpoint field dereference should be possible" pvl """ + """, + ) + + choreography( + desc = "plain endpoint field dereference should be possible", + flag = "--generate-permissions", + fail = "assertFailed:false", + pvl = """ class Storage { int x; } @@ -76,19 +103,25 @@ class TechnicalVeyMontSpec extends VercorsSpec { assert alice.x == 0; } } - """) + """, + ) - vercors should error withCode "noSuchName" in - "non-existent thread name in communicate fails" pvl """ + choreography( + error = "choreography:noSuchName", + desc = "non-existent thread name in communicate fails", + pvl = """ choreography Example() { run { communicate charlie.x <- charlie.x; } } - """ + """, + ) - vercors should error withCode "noSuchName" in - "non-existent field in communicate fails" pvl """ + choreography( + error = "choreography:noSuchName", + desc = "non-existent field in communicate fails", + pvl = """ class Storage { int x; } choreography Example() { endpoint charlie = Storage(); @@ -96,10 +129,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate charlie.nonExistent <- charlie.nonExistent; } } - """ + """, + ) - vercors should error withCode "parseError" in - "parameterized sends not yet supported " pvl """ + choreography( + error = "choreography:parseError", + desc = "parameterized sends not yet supported", + pvl = """ class Storage { int x; } choreography Example() { endpoint alice[10] = Storage(); @@ -108,22 +144,31 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate alice[i: 0 .. 9].x <- bob[i + 1].y; } } - """ + """, + ) - vercors should error withCode "noRunMethod" in - "run method should always be present" pvl """ + choreography( + error = "choreography:noRunMethod", + desc = "run method should always be present", + pvl = """ choreography Example() { } - """ + """, + ) - vercors should error withCode "parseError" in - "endpoints can only have class types" pvl """ + choreography( + error = "choreography:parseError", + desc = "endpoints can only have class types", + pvl = """ choreography Example() { endpoint alice = int(); } - """ + """, + ) - (vercors should verify using silicon flag "--veymont-generate-permissions" in - "Endpoint fields should be assignable" pvl """ + choreography( + flag = "--generate-permissions", + desc = "Endpoint fields should be assignable", + pvl = """ class Storage { int x; int y; } choreography Example() { endpoint alice = Storage(); @@ -132,49 +177,62 @@ class TechnicalVeyMontSpec extends VercorsSpec { alice.x := alice.y; } } - """) + """, + ) - vercors should error withCode "resolutionError:seqProgInstanceMethodArgs" in - "instance method in choreography cannot have arguments" pvl """ + choreography( + error = "choreography:resolutionError:seqProgInstanceMethodArgs", + desc = "instance method in choreography cannot have arguments", + pvl = """ choreography Example() { void m(int x) { } run { } } - """ + """, + ) - vercors should error withCode "resolutionError:seqProgInstanceMethodBody" in - "instance method in choreography must have a body" pvl """ + choreography( + error = "choreography:resolutionError:seqProgInstanceMethodBody", + desc = "instance method in choreography must have a body", + pvl = """ choreography Example() { void m(); run { } } - """ + """, + ) - vercors should error withCode - "resolutionError:seqProgInstanceMethodNonVoid" in - "instance method in choreography must have void return type" pvl """ + choreography( + error = "choreography:resolutionError:seqProgInstanceMethodNonVoid", + desc = "instance method in choreography must have void return type", + pvl = """ choreography Example() { int m() { } run { } } - """ + """, + ) - vercors should error withCode "resolutionError:chorStatement" in - "`choreography` excludes certain statements" pvl """ + choreography( + error = "choreography:resolutionError:chorStatement", + desc = "`choreography` excludes certain statements", + pvl = """ class C { } choreography Example(C c) { run { lock c; } } - """ + """, + ) - vercors should verify using silicon in - "Dereferencing other endpoints in arguments is possible if permissions are available for the endpoint context" pvl - """ + choreography( + desc = + "Dereferencing other endpoints in arguments is possible if permissions are available for the endpoint context", + pvl = """ class C { C d; void foo(int x); int x; } choreography Example(C c) { endpoint c = C(); @@ -184,11 +242,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { c.foo(d.x); } } - """ - - vercors should fail withCode "perm" using silicon in - "Dereferencing other endpoints in arguments is not possible if permissions are not available for the endpoint context" pvl - """ + """, + ) + + choreography( + fail = "perm", + desc = + "Dereferencing other endpoints in arguments is not possible if permissions are not available for the endpoint context", + pvl = """ class C { C d; void foo(int x); int x; } choreography Example(C c) { endpoint c = C(); @@ -198,19 +259,24 @@ class TechnicalVeyMontSpec extends VercorsSpec { c.foo(d.x); } } - """ + """, + ) - vercors should verify using silicon in "Empty choreography must verify" pvl - """ + choreography( + desc = "Empty choreography must verify", + pvl = """ choreography C() { run { } } - """ + """, + ) - vercors should error withCode "resolutionError:type" in - "Assign must be well-typed" pvl """ + choreography( + error = "choreography:resolutionError:type", + desc = "Assign must be well-typed", + pvl = """ class C { int x; } choreography C() { endpoint charlie = C(); @@ -218,10 +284,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { charlie.x := true; } } - """ + """, + ) - vercors should error withCode "resolutionError:type" in - "Communicating parties must agree on the type" pvl """ + choreography( + error = "choreography:resolutionError:type", + desc = "Communicating parties must agree on the type", + pvl = """ class C { int c; } class A { bool a; } choreography C() { @@ -231,10 +300,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate charlie.c <- alice.a; } } - """ + """, + ) - (vercors should verify using silicon flag "--veymont-generate-permissions" in - "assignment should work" pvl """ + choreography( + flag = "--generate-permissions", + desc = "assignment should work", + pvl = """ class Storage { int x; @@ -252,10 +324,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { assert alice.x == 0; } } - """) - - (vercors should fail withCode "postFailed:false" using silicon flag - "--veymont-generate-permissions" in "Postcondition of run can fail" pvl """ + """, + ) + + choreography( + fail = "postFailed:false", + flag = "--generate-permissions", + desc = "Postcondition of run can fail", + pvl = """ class Storage { int x; } @@ -266,11 +342,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { run { } } - """) - - (vercors should fail withCode "postFailed:false" using silicon flag - "--veymont-generate-permissions" in - "Postcondition of choreography can fail" pvl """ + """, + ) + + choreography( + fail = "postFailed:false", + flag = "--generate-permissions", + desc = "Postcondition of choreography can fail", + pvl = """ class Storage { int x; } @@ -282,12 +361,15 @@ class TechnicalVeyMontSpec extends VercorsSpec { run { } } - """) - - vercors should fail withCode "perm" using silicon flag - "--veymont-generate-permissions" in - "Assignment statement only allows one endpoint in the assigned expression" pvl - """ + """, + ) + + choreography( + fail = "perm", + flag = "--generate-permissions", + desc = + "Assignment statement only allows one endpoint in the assigned expression", + pvl = """ class Storage { int x; } @@ -299,11 +381,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { alice.x := bob.x; } } - """ - - (vercors should fail withCode "branchNotUnanimous" using silicon flag - "--veymont-generate-permissions" in - "Parts of condition in branch have to agree inside seqprog" pvl """ + """, + ) + + choreography( + fail = "branchNotUnanimous", + flag = "--generate-permissions", + desc = "Parts of condition in branch have to agree inside seqprog", + pvl = """ class Storage { int x; } @@ -317,12 +402,15 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) - - (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 - """ + """, + ) + + choreography( + fail = "branchNotUnanimous", + flag = "--generate-permissions", + desc = + "Parts of condition in branch have to agree inside seqprog, including conditions for all endpoints", + pvl = """ class Storage { int x; } @@ -339,11 +427,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) - - (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 - """ + """, + ) + + choreography( + flag = "--generate-permissions", + desc = + "If there is only one endpoint, the conditions don't have to agree, as there is only one endpoint", + pvl = """ class Storage { int x; } @@ -359,10 +450,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) + """, + ) - vercors should error withCode "seqProgParticipantErrors" in - "`if` cannot depend on bob, inside an `if` depending on alice" pvl """ + choreography( + error = "choreography:seqProgParticipantErrors", + desc = "`if` cannot depend on bob, inside an `if` depending on alice", + pvl = """ class Storage { int x; } @@ -378,10 +472,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """ + """, + ) - vercors should error withCode "seqProgParticipantErrors" in - "If alice branches, bob cannot communicate" pvl """ + choreography( + error = "choreography:seqProgParticipantErrors", + desc = "If alice branches, bob cannot communicate", + pvl = """ class Storage { int x; } @@ -395,10 +492,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """ + """, + ) - vercors should error withCode "seqProgParticipantErrors" in - "If alice branches, bob cannot assign" pvl """ + choreography( + error = "choreography:seqProgParticipantErrors", + desc = "If alice branches, bob cannot assign", + pvl = """ class Storage { int x; } @@ -412,10 +512,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """ + """, + ) - (vercors should verify using silicon flag "--veymont-generate-permissions" in - "Programs where branch conditions agree should verify" pvl """ + choreography( + flag = "--generate-permissions", + desc = "Programs where branch conditions agree should verify", + pvl = """ class Storage { bool x; } @@ -432,12 +535,15 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) - - (vercors should fail withCode "loopUnanimityNotEstablished" using silicon flag - "--veymont-generate-permissions" in - "Programs where branch condition unanimity cannot be established should fail" pvl - """ + """, + ) + + choreography( + fail = "loopUnanimityNotEstablished", + flag = "--generate-permissions", + desc = + "Programs where branch condition unanimity cannot be established should fail", + pvl = """ class Storage { bool x; } @@ -451,12 +557,15 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) - - (vercors should fail withCode "loopUnanimityNotMaintained" using silicon flag - "--veymont-generate-permissions" in - "Programs where branch condition unanimity cannot be maintained should fail" pvl - """ + """, + ) + + choreography( + fail = "loopUnanimityNotMaintained", + flag = "--generate-permissions", + desc = + "Programs where branch condition unanimity cannot be maintained should fail", + pvl = """ class Storage { bool x; } @@ -472,10 +581,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) + """, + ) - vercors should error withCode "seqProgParticipantErrors" in - "Loops should also limit the number of participants" pvl """ + choreography( + error = "choreography:seqProgParticipantErrors", + desc = "Loops should also limit the number of participants", + pvl = """ class Storage { bool x; } @@ -493,11 +605,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """ - - (vercors should verify using silicon flag "--veymont-generate-permissions" in - "Loops should also limit the number of participants when combined with branches" pvl - """ + """, + ) + + choreography( + flag = "--generate-permissions", + desc = + "Loops should also limit the number of participants when combined with branches", + pvl = """ class Storage { bool x; } @@ -517,11 +632,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) - - vercors should error withCode "seqProgParticipantErrors" in - "Loops should also limit the number of participants when combined with branches, failing" pvl - """ + """, + ) + + choreography( + error = "choreography:seqProgParticipantErrors", + desc = + "Loops should also limit the number of participants when combined with branches, failing", + pvl = """ class Storage { bool x; } @@ -542,10 +660,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """ + """, + ) - (vercors should verify using silicon flag "--veymont-generate-permissions" in - "Permission should be generated for constructors as well" pvl """ + choreography( + flag = "--generate-permissions", + desc = "Permission should be generated for constructors as well", + pvl = """ class Storage { int x; @@ -562,11 +683,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { assert alice.x == 2; } } - """) - - (vercors should fail withCode "perm" using silicon in - "When no permission is generated, a failure should occur on endpoint field access" pvl - """ + """, + ) + + choreography( + fail = "perm", + desc = + "When no permission is generated, a failure should occur on endpoint field access", + pvl = """ class Storage { int x; } @@ -578,11 +702,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate alice.x <- bob.x; } } - """) - - (vercors should fail withCode "perm" using silicon in - "When no permission is generated, a failure should occur on seq assign field access" pvl - """ + """, + ) + + choreography( + fail = "perm", + desc = + "When no permission is generated, a failure should occur on seq assign field access", + pvl = """ class Storage { int x; } @@ -593,11 +720,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { 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 - """ + """, + ) + + choreography( + flag = "--generate-permissions", + desc = + "Permissions are generated for loop invariants, procedures, functions, instance methods, instance functions", + pvl = """ class Storage { int x; @@ -639,11 +769,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { alice.all(); } } - """) - - (vercors should verify using silicon flag "--veymont-generate-permissions" in - "Permission generation should only generate permissions that are strictly necessary" pvl - """ + """, + ) + + choreography( + flag = "--generate-permissions", + desc = + "Permission generation should only generate permissions that are strictly necessary", + pvl = """ class Storage { int x; } @@ -661,13 +794,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { assert bob.x == 3; } } - """) + """, + ) // Auxiliary methods turned off indefinitely for now. Though can be implemented with just engineering work. // (vercors // should verify // using silicon -// flag "--veymont-generate-permissions" +// flag "--generate-permissions" // in "Calling auxiliary methods in seq_prog should be possible" // pvl // """ @@ -693,7 +827,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { // (vercors // should verify // using silicon -// flag "--veymont-generate-permissions" +// flag "--generate-permissions" // in "VeyMont should conservatively generate permissions for auxiliary methods" // pvl // """ @@ -723,7 +857,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { // should fail // withCode "assertFailed:false" // using silicon -// flag "--veymont-generate-permissions" +// flag "--generate-permissions" // in "Permissions should be generated when an endpoint participates in an auxiliary method" // pvl // """ @@ -750,8 +884,10 @@ class TechnicalVeyMontSpec extends VercorsSpec { // } // """) - (vercors should fail withCode "chorRunPreFailed:false" using silicon in - "Precondition of run should be checked" pvl """ + choreography( + fail = "chorRunPreFailed:false", + desc = "Precondition of run should be checked", + pvl = """ class C { } choreography Example(int x) { endpoint c = C(); @@ -759,10 +895,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { run { } } - """) + """, + ) - (vercors should fail withCode "postFailed:false" using silicon in - "Precondition of run is never witnessed if there are no endpoints" pvl """ + choreography( + fail = "postFailed:false", + desc = "Precondition of run is never witnessed if there are no endpoints", + pvl = """ ensures x == 0; choreography Example(int x) { requires x == 0; @@ -770,10 +909,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { run { } } - """) + """, + ) - (vercors should fail withCode "preFailed:false" using silicon in - "Precondition of endpoint constructor should be checked" pvl """ + choreography( + fail = "preFailed:false", + desc = "Precondition of endpoint constructor should be checked", + pvl = """ class Storage { requires x == 0; constructor (int x) { } @@ -785,10 +927,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { run { } } - """) + """, + ) - (vercors should error withCode "resolutionError:chorStatement" in - "Assignment should not be allowed in choreographies" pvl """ + choreography( + error = "choreography:resolutionError:chorStatement", + desc = "Assignment should not be allowed in choreographies", + pvl = """ class Storage { int x; } @@ -799,11 +944,14 @@ class TechnicalVeyMontSpec extends VercorsSpec { alice.x = 0; } } - """) - - (vercors should fail withCode "participantsNotDistinct" using silicon flag - "--veymont-generate-permissions" in - "Endpoints participating in a communicate should be distinct" pvl """ + """, + ) + + choreography( + fail = "participantsNotDistinct", + flag = "--generate-permissions", + desc = "Endpoints participating in a communicate should be distinct", + pvl = """ class Storage { int x; } @@ -814,15 +962,19 @@ class TechnicalVeyMontSpec extends VercorsSpec { communicate alice.x <- alice.x; } } - """) + """, + ) // Disabled indefinitely until EncodePermissionStratification.scala is refactored to fully support generics // vercors should verify using silicon flag -// "--veymont-generate-permissions" example +// "--generate-permissions" example // "technical/veymont/genericEndpoints.pvl" - (vercors should fail withCode "branchNotUnanimous" using silicon flag - "--veymont-generate-permissions" in "branch unanimity for if" pvl """ + choreography( + fail = "branchNotUnanimous", + flag = "--generate-permissions", + desc = "branch unanimity for if", + pvl = """ class Storage { int x; } @@ -838,10 +990,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { } } } - """) + """, + ) - vercors should fail withCode "perm" using silicon in - "deref should be safe" pvl """ + choreography( + fail = "perm", + desc = "deref should be safe", + pvl = """ class Storage { int x; int y; } choreography runPostFails() { @@ -851,10 +1006,13 @@ class TechnicalVeyMontSpec extends VercorsSpec { alice.x := alice.y; } } - """ + """, + ) - vercors should fail withCode "perm" using silicon in - "assigning to a deref should fail if there is no permission" pvl """ + choreography( + fail = "perm", + desc = "assigning to a deref should fail if there is no permission", + pvl = """ class Storage { int x; int y; } choreography runPostFails() { endpoint alice = Storage(); @@ -863,10 +1021,12 @@ class TechnicalVeyMontSpec extends VercorsSpec { alice.x := alice.y; } } - """ + """, + ) - vercors should verify using silicon in - "assigning to a deref should succeed if there is permission" pvl """ + choreography( + desc = "assigning to a deref should succeed if there is permission", + pvl = """ class Storage { int x; int y; } choreography runPostFails() { endpoint alice = Storage(); @@ -875,67 +1035,103 @@ class TechnicalVeyMontSpec extends VercorsSpec { alice.x := alice.y; } } - """ + """, + ) val wd = "technical/veymont" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$wd/checkLTS/ltstest.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$wd/checkLTS/simpleifelse.pvl" - - (vercors should error withCode "resolutionError:seqProgInvocation" flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl") - (vercors should error withCode "seqProgParticipantErrors" example - s"$wd/checkMainSyntaxAndWellFormedness/IfCondition.pvl") - - (vercors should verify using silicon flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/MainConstructorWithArgs.pvl") + choreography( + flag = "--generate-permissions", + input = example(s"$wd/checkLTS/ltstest.pvl"), + ) + + choreography( + flag = "--generate-permissions", + input = example(s"$wd/checkLTS/simpleifelse.pvl"), + ) + + choreography( + error = "choreography:resolutionError:seqProgInvocation", + flag = "--generate-permissions", + input = example(s"$wd/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl"), + ) + + choreography( + error = "choreography:seqProgParticipantErrors", + input = example(s"$wd/checkMainSyntaxAndWellFormedness/IfCondition.pvl"), + ) + + choreography( + flag = "--generate-permissions", + input = example( + s"$wd/checkMainSyntaxAndWellFormedness/MainConstructorWithArgs.pvl" + ), + ) // Disabled indefinitely while submethods are not supported. // vercors should verify using silicon flag - // "--veymont-generate-permissions" example + // "--generate-permissions" example // s"$wd/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl" - - (vercors should error withCode "resolutionError:seqProgInvocation" flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl") - - (vercors should error withCode "resolutionError:seqProgInvocation" flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl") - - (vercors should error withCode "resolutionError:seqProgEndpointAssign" flags - ("--veymont-generate-permissions", "--dev-veymont-allow-assign") example - s"$wd/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl") - - (vercors should error withCode "resolutionError:chorStatement" flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/WaitStatement.pvl") - - (vercors should fail withCode "loopUnanimityNotMaintained" using silicon flag - "--veymont-generate-permissions" example - s"$wd/checkMainSyntaxAndWellFormedness/WhileCondition.pvl") - - vercors should verify using silicon flag - "--veymont-generate-permissions" example - s"$wd/checkTypesNonMain/RoleFieldType2.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example - s"$wd/checkTypesNonMain/RoleMethodType4.pvl" - - vercors should verify using silicon example s"$wd/first.pvl" - vercors should verify using silicon flag - "--veymont-generate-permissions" example s"$wd/subFieldAssign.pvl" - vercors should fail withCode "perm" using silicon example - s"$wd/subFieldAssignError.pvl" - + choreography( + flag = "--generate-permissions", + input = example( + s"$wd/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl" + ), + ) + choreography( + flag = "--generate-permissions", + input = example(s"$wd/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl"), + ) + + choreography( + error = "choreography:resolutionError:seqProgInvocation", + flag = "--generate-permissions", + input = example( + s"$wd/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl" + ), + ) + + choreography( + error = "choreography:resolutionError:seqProgInvocation", + flag = "--generate-permissions", + input = example(s"$wd/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl"), + ) + + choreography( + error = "choreography:resolutionError:seqProgEndpointAssign", + flags = Seq("--generate-permissions", "--dev-veymont-allow-assign"), + input = example( + s"$wd/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl" + ), + ) + + choreography( + error = "choreography:resolutionError:chorStatement", + flag = "--generate-permissions", + input = example(s"$wd/checkMainSyntaxAndWellFormedness/WaitStatement.pvl"), + ) + + choreography( + fail = "loopUnanimityNotMaintained", + flag = "--generate-permissions", + input = example(s"$wd/checkMainSyntaxAndWellFormedness/WhileCondition.pvl"), + ) + + choreography( + flag = "--generate-permissions", + input = example(s"$wd/checkTypesNonMain/RoleFieldType2.pvl"), + ) + choreography( + flag = "--generate-permissions", + input = example(s"$wd/checkTypesNonMain/RoleMethodType4.pvl"), + ) + + choreography(input = example(s"$wd/first.pvl")) + + choreography( + flag = "--generate-permissions", + input = example(s"$wd/subFieldAssign.pvl"), + ) + + choreography(fail = "perm", input = example(s"$wd/subFieldAssignError.pvl")) } diff --git a/test/main/vct/test/integration/examples/veymont/VeyMontExamplesSpec.scala b/test/main/vct/test/integration/examples/veymont/VeyMontExamplesSpec.scala index 154ac6a015..dbf41a9489 100644 --- a/test/main/vct/test/integration/examples/veymont/VeyMontExamplesSpec.scala +++ b/test/main/vct/test/integration/examples/veymont/VeyMontExamplesSpec.scala @@ -1,37 +1,56 @@ package vct.test.integration.examples.veymont -import vct.test.integration.helper.VercorsSpec +import vct.test.integration.helper.VeyMontSpec -class VeyMontExamplesSpec extends VercorsSpec { +class VeyMontExamplesSpec extends VeyMontSpec { { val wd = "concepts/veymont/generatedPermissions" - vercors should verify using silicon flags - "--veymont-generate-permissions" examples - ( + + choreography( + desc = "Tic-Tac-Toe (generated permissions)", + inputs = examples( s"$wd/TicTacToe/Player.pvl", s"$wd/TicTacToe/Move.pvl", s"$wd/TicTacToe/TicTacToe.pvl", - ) - - vercors should verify using silicon flags - "--veymont-generate-permissions" example s"$wd/leaderelectring.pvl" - - vercors should verify using silicon flags - "--veymont-generate-permissions" example s"$wd/leaderelectstar.pvl" - - vercors should verify using silicon flags - "--veymont-generate-permissions" example s"$wd/paperscissorsrock.pvl" - - vercors should verify using silicon flags - "--veymont-generate-permissions" example s"$wd/parallel_while.pvl" + ), + flags = Seq("--generate-permissions"), + ) + + choreography( + desc = "Leader elect ring (generated permissions)", + inputs = examples(s"$wd/leaderelectring.pvl"), + flags = Seq("--generate-permissions"), + ) + + choreography( + desc = "Leader elect star (generated permissions)", + inputs = examples(s"$wd/leaderelectstar.pvl"), + flags = Seq("--generate-permissions"), + ) + + choreography( + desc = "Paper-scissors-rock (generated permissions)", + inputs = examples(s"$wd/paperscissorsrock.pvl"), + flags = Seq("--generate-permissions"), + ) + + choreography( + desc = "Parallel while (generated permissions)", + inputs = examples(s"$wd/parallel_while.pvl"), + flags = Seq("--generate-permissions"), + ) // Disabled indefinitely until submethods are enabled again // vercors should verify using silicon flags - // "--veymont-generate-permissions" example s"$wd/spectral_norm.pvl" + // "--generate-permissions" example s"$wd/spectral_norm.pvl" } { val wd = "concepts/veymont/annotatedPermissions" - vercors should verify using silicon example s"$wd/swap.pvl" + + choreography( + desc = "Swap (annotated permissions)", + inputs = examples(s"$wd/swap.pvl"), + ) } } diff --git a/test/main/vct/test/integration/examples/veymont/VeyMontPermissionsPaperSpec.scala b/test/main/vct/test/integration/examples/veymont/VeyMontPermissionsPaperSpec.scala deleted file mode 100644 index d96b621789..0000000000 --- a/test/main/vct/test/integration/examples/veymont/VeyMontPermissionsPaperSpec.scala +++ /dev/null @@ -1,25 +0,0 @@ -package vct.test.integration.examples.veymont - -import vct.test.integration.helper.VercorsSpec - -class VeyMontPermissionsPaperSpec extends VercorsSpec { - val wd = "concepts/veymont/FM2024 - VeyMont" - - vercors should verify using silicon flags - "--veymont-generate-permissions" examples - (s"$wd/0-TTT/Move.pvl", s"$wd/0-TTT/Player.pvl", s"$wd/0-TTT/TTT.pvl") - - vercors should verify using silicon flags "--dev-unsafe-optimization" examples - ( - s"$wd/1-TTTmsg/Move.pvl", - s"$wd/1-TTTmsg/Player.pvl", - s"$wd/1-TTTmsg/1-TTTmsg.pvl", - ) - - vercors should verify using silicon flags "--dev-unsafe-optimization" examples - ( - s"$wd/2-TTTlast/Move.pvl", - s"$wd/2-TTTlast/Player.pvl", - s"$wd/2-TTTlast/2-TTTlast.pvl", - ) -} diff --git a/test/main/vct/test/integration/helper/ExampleFiles.scala b/test/main/vct/test/integration/helper/ExampleFiles.scala index fb2d8278c6..09d263d361 100644 --- a/test/main/vct/test/integration/helper/ExampleFiles.scala +++ b/test/main/vct/test/integration/helper/ExampleFiles.scala @@ -9,9 +9,6 @@ case object ExampleFiles { "examples/private/", "examples/archive/", "examples/concepts/resourceValues", - // TODO (RR): The next two can be deleted when the veymont permissions paper artefact is finished - "examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/TTTmsg-generatedImplementation.pvl", - "examples/concepts/veymont/FM2024 - VeyMont/2-TTTlast/TTTlast-generated.pvl", ).map(_.replaceAll("/", File.separator)) val IGNORE_EXTS: Seq[String] = Seq(".h", ".bib", ".xml") diff --git a/test/main/vct/test/integration/helper/VercorsSpec.scala b/test/main/vct/test/integration/helper/VercorsSpec.scala index aa3979168e..4e65b9dc8a 100644 --- a/test/main/vct/test/integration/helper/VercorsSpec.scala +++ b/test/main/vct/test/integration/helper/VercorsSpec.scala @@ -242,4 +242,18 @@ abstract class VercorsSpec extends AnyFlatSpec { val silicon: Seq[Backend] = Seq(types.Backend.Silicon) val carbon: Seq[Backend] = Seq(types.Backend.Carbon) val anyBackend: Seq[Backend] = Seq(types.Backend.Silicon, types.Backend.Carbon) + + def example(p: Path): Path = { + val path = Paths.get("examples").resolve(p) + coveredExamples ++= Seq(path) + path + } + + def example(p: String): Path = example(Paths.get(p)) + + def examples(p: String*): Seq[Path] = + p.map(example) + + def examplePaths(p: Path*): Seq[Path] = + p.map(example) } diff --git a/test/main/vct/test/integration/helper/VeyMontSpec.scala b/test/main/vct/test/integration/helper/VeyMontSpec.scala new file mode 100644 index 0000000000..71570a0de0 --- /dev/null +++ b/test/main/vct/test/integration/helper/VeyMontSpec.scala @@ -0,0 +1,227 @@ +package vct.test.integration.helper + +import ch.qos.logback.classic.{Level, Logger} +import com.typesafe.scalalogging.LazyLogging +import hre.io.LiteralReadable +import hre.util.FilesHelper +import org.scalactic.source +import org.scalatest.Tag +import org.scalatest.concurrent.TimeLimits.failAfter +import org.scalatest.time.{Seconds, Span} +import org.slf4j.LoggerFactory +import vct.col.origin.VerificationFailure +import vct.main.modes.VeyMont.StageResult +import vct.main.modes.VeyMont +import vct.options.types.PathOrStd +import vct.options.Options +import vct.result.VerificationError +import vct.result.VerificationError.{SystemError, UserError} +import vct.test.integration.helper.{ResultModel => R} +import vct.test.integration.helper.VercorsSpec.MATRIX_COUNT + +import java.nio.file.{Path, Paths} + +sealed trait ResultModel +object ResultModel { + def ofTestSpec( + fail: String, + fails: Seq[String], + error: String, + ): ResultModel = { + assert(!(fail != null && error != null && fails != null)) + (fail, fails, error) match { + case (null, null, null) => Pass + case (fail, null, null) => Fail(Seq(fail)) + case (null, fails, null) => Fail(fails) + case (null, null, error) => Error(error) + case _ => ??? + } + } + + def ofFailure(fails: Seq[VerificationFailure]): ResultModel = + if (fails.isEmpty) + Pass + else + Fail(fails.map(_.code)) + + def ofFrontendOutput( + res: Either[VerificationError, StageResult] + ): ResultModel = + res match { + case Left(error: UserError) => Error(error.code) + case Left(crash: SystemError) => Crash(crash) + case Right(stageResult) => + stageResult match { + case VeyMont.ChoreographyResult(_, fails) => ofFailure(fails) + case VeyMont.GenerateResult(_) => Pass + case VeyMont.ImplementationResult(fails) => ofFailure(fails) + } + } + + case class Fail(codes: Seq[String]) extends ResultModel { + require(codes.nonEmpty) + } + case class Error(code: String) extends ResultModel + case class Crash(err: SystemError) extends ResultModel + case object Pass extends ResultModel +} + +class VeyMontSpec extends VercorsSpec with LazyLogging { + sealed trait Language + case object Pvl extends Language + case object Java extends Language + + def choreography( + pvl: String = null, + input: Path = null, + inputs: Seq[Path] = null, + desc: String = null, + flags: Seq[String] = Seq(), + flag: String = null, + fail: String = null, + fails: Seq[String] = null, + error: String = null, + targetLanguage: Language = Pvl, + )(implicit pos: source.Position): Unit = + veymontTest( + pvl = pvl, + desc = desc, + input = input, + inputs = inputs, + flags = "--choreography" +: flags, + flag = flag, + fail = fail, + fails = fails, + error = error, + targetLanguage = targetLanguage, + ) + + def implementation( + pvl: String = null, + desc: String = null, + input: Path = null, + inputs: Seq[Path] = null, + flags: Seq[String] = Seq(), + flag: String = null, + fail: String = null, + fails: Seq[String] = null, + error: String = null, + targetLanguage: Language = Pvl, + )(implicit pos: source.Position): Unit = + veymontTest( + pvl = pvl, + desc = desc, + input = input, + inputs = inputs, + flags = Seq("--implementation") ++ flags, + flag = flag, + fail = fail, + fails = fails, + error = error, + targetLanguage = targetLanguage, + ) + + def veymontTest( + pvl: String = null, + input: Path = null, + inputs: Seq[Path] = null, + desc: String = null, + fail: String = null, + fails: Seq[String] = null, + error: String = null, + flag: String = null, + flags: Seq[String] = Seq(), + targetLanguage: Language = Pvl, + processImplementation: Path => Unit = null, + )(implicit pos: source.Position): Unit = { + // First combine both the single and the sequence input. + // Using them both is a weird use case but supporting it is okay + val pathInputs = Option(input).toSeq ++ Option(inputs).toSeq.flatten + + // When giving a pvl literal, there should also be a description + // Otherwise, inputs should be non-null, so a description can be derived if necessary + require((pvl != null && desc != null) || pathInputs != Seq()) + val descr = + if (desc == null) + s"Files ${pathInputs.mkString(",")}" + else + desc + // Also, either there have to be inputs, or a pvl literal, but not both + require(pathInputs == Seq() ^ (pvl == null)) + + val actualInputs = + (pathInputs, pvl) match { + case (inputs, null) => + require(inputs.nonEmpty) + // Register examples in the test suite + val absoluteExamplePath = Paths.get("examples").toAbsolutePath + inputs.foreach { p => + if (p.toAbsolutePath.startsWith(absoluteExamplePath)) { + coveredExamples ++= Seq(p) + } + } + inputs.map(PathOrStd.Path) + case (Seq(), pvl) => Seq(LiteralReadable("test.pvl", pvl)) + } + + val fullDesc: String = s"${descr.capitalize} verifies with silicon" + // PB: note that object typically do not have a deterministic hashCode, but Strings do. + val matrixId = Math.floorMod(fullDesc.hashCode, MATRIX_COUNT) + val matrixTag = Tag(s"MATRIX[$matrixId]") + + registerTest(fullDesc, Tag("MATRIX"), matrixTag) { + LoggerFactory.getLogger("viper").asInstanceOf[Logger].setLevel(Level.OFF) + LoggerFactory.getLogger("vct").asInstanceOf[Logger].setLevel(Level.INFO) + + FilesHelper.withTempDir { temp => + val tempSource = { + targetLanguage match { + case Pvl => temp.resolve("output.pvl") + case Java => temp.resolve("output.java") + } + } + + val outputFlags = + if (processImplementation != null) { + Seq("--veymont-output", tempSource.toString) + } else + Seq() + + failAfter(Span(300, Seconds)) { + val expectedResult = ResultModel.ofTestSpec(fail, fails, error) + val actualResult = ResultModel.ofFrontendOutput(VeyMont.ofOptions( + Options.parse( + (Seq("--veymont") ++ outputFlags ++ flags ++ Option(flag).toSeq) + .toArray + ).get, + actualInputs, + )) + + processResult(expectedResult, actualResult) + + Option(processImplementation).foreach(f => f(tempSource)) + } + } + } + } + + def processResult(expected: ResultModel, actual: ResultModel): Unit = { + info(s"Expected: $expected") + info(s"Actual: $actual") + + def show(res: ResultModel): String = + res match { + case R.Fail(Seq(code)) => s"fail with code $code" + case R.Fail(codes) => + s"fail with codes: ${codes.mkString("- ", "\n- ", "")}" + case R.Error(code) => s"error with code $code" + case R.Crash(err) => s"crash with message:\n${err.text}" + case R.Pass => "pass" + } + + assert( + expected == actual, + s"Expected test result: ${show(expected)}\nActual test result: ${show(actual)}", + ) + } +} diff --git a/test/main/vct/test/integration/meta/ExampleCoverage.scala b/test/main/vct/test/integration/meta/ExampleCoverage.scala index e5918fb39d..668b5e9c94 100644 --- a/test/main/vct/test/integration/meta/ExampleCoverage.scala +++ b/test/main/vct/test/integration/meta/ExampleCoverage.scala @@ -2,7 +2,7 @@ package vct.test.integration.meta import org.scalatest.flatspec.AnyFlatSpec import vct.test.integration.examples._ -import vct.test.integration.examples.veymont.{FM2023VeyMontSpec, TechnicalVeyMontSpec, VeyMontExamplesSpec, VeyMontPermissionsPaperSpec} +import vct.test.integration.examples.veymont.{FM2023VeyMontSpec, TechnicalVeyMontSpec, VeyMontExamplesSpec, IFM2024VeyMontPermissionsSpec} import vct.test.integration.helper._ class ExampleCoverage extends AnyFlatSpec { @@ -60,7 +60,7 @@ class ExampleCoverage extends AnyFlatSpec { new VerifyThisSpec(), new FM2023VeyMontSpec(), new VeyMontExamplesSpec(), - new VeyMontPermissionsPaperSpec(), + new IFM2024VeyMontPermissionsSpec(), new WaitNotifySpec(), new WandSpec(), new AutoValueSpec(),