Skip to content

Commit

Permalink
Resolve problems in other veymont test suites
Browse files Browse the repository at this point in the history
  • Loading branch information
bobismijnnaam committed May 31, 2024
1 parent 13bbbcc commit 1d24a5e
Show file tree
Hide file tree
Showing 10 changed files with 86 additions and 84 deletions.
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
class Player {
int c00, c01, c02, c10, c11, c12, c20, c21, c22;
int myToken;
Move move, temp;
Move move;
boolean turn;


Expand All @@ -25,7 +25,6 @@ class Player {
myToken = tok;
turn = t;
move = new Move(0, 0, tok);
temp = new Move(-1, -1, -1);
}


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,24 +7,20 @@ choreography TTT() {
endpoint p1 = Player(0, true);
endpoint p2 = Player(1, false);

context ticTacToeAnnotations(p1, p2);
context (\chor ticTacToeAnnotations(p1, p2));
ensures p1.gameFinished() && p2.gameFinished();
run {
loop_invariant ticTacToeAnnotations(p1, p2);
loop_invariant !p1.gameFinished() == !p2.gameFinished();
loop_invariant (\chor ticTacToeAnnotations(p1, p2));
loop_invariant (\chor !p1.gameFinished() == !p2.gameFinished());
while(!p1.gameFinished() && !p2.gameFinished()) {
// TODO (RR): Re-enable with in_chor
// assert p1.turn == !p2.turn;
if(p1.turn && !p2.turn) {
p1.createNewMove();
p1.temp := p1.move.clone();
communicate p2.move <- p1.temp;
p1.temp := new Move(-1, -1, -1); // TODO (RR): Workaround for not having memory management, delete when we support exprs in communicate
communicate p2.move <- p1.move.clone();
} else {
p2.createNewMove();
p2.temp := p2.move.clone();
communicate p1.move <- p2.temp;
p2.temp := new Move(-1, -1, -1); // TODO (RR): Workaround for not having memory management, delete when we support exprs in communicate
communicate p1.move <- p2.move.clone();
}
p1.doMove();
p2.doMove();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ choreography leaderElectRing() {
ensures c.maxVal == c.maxVal(a.rank,b.rank,d.rank,c.rank);
ensures c.maxVal == a.rank || c.maxVal == b.rank || c.maxVal == c.rank || c.maxVal == d.rank;
run {
loop_invariant a.rank == \old(a.rank) ** b.rank == \old(b.rank) ** c.rank == \old(c.rank) ** d.rank == \old(d.rank);
loop_invariant a.rank == \old(a.rank) ** b.rank == \old(b.rank) ** c.rank == \old(c.rank) ** d.rank == \old(d.rank);
loop_invariant a.rank != b.rank && a.rank != c.rank && a.rank != d.rank && b.rank != c.rank && b.rank != d.rank && c.rank != d.rank;
loop_invariant 0 <= c.n && c.n <= 3;
loop_invariant a.n == c.n && b.n == c.n && d.n == c.n;
Expand All @@ -49,7 +49,7 @@ choreography leaderElectRing() {
loop_invariant c.n == 3 ==> a.maxVal == a.maxVal(a.rank,b.rank,c.rank,d.rank);
loop_invariant c.n == 3 ==> b.maxVal == b.maxVal(a.rank,b.rank,c.rank,d.rank);
loop_invariant c.n == 3 ==> c.maxVal == c.maxVal(a.rank,b.rank,c.rank,d.rank);
loop_invariant c.n == 3 ==> d.maxVal == d.maxVal(a.rank,b.rank,c.rank,d.rank);
loop_invariant c.n == 3 ==> d.maxVal == d.maxVal(a.rank,b.rank,c.rank,d.rank);
while(a.n < 3 && b.n < 3 && c.n < 3 && d.n < 3) {
communicate a.left <- d.maxVal;
communicate b.left <- a.maxVal;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
choreography Main() {
endpoint a = Role(5);
endpoint b = Role(6);
endpoint c = Role(7);
endpoint a = Role(5);
endpoint b = Role(6);
endpoint c = Role(7);

requires a.x == 5 && b.x == 6 && c.x == 7;
requires a.x == 5 && b.x == 6 && c.x == 7;
run {
while(a.x >= 5 && b.x == 6 && c.x == 7) {
c.x := -2;
Expand Down
2 changes: 1 addition & 1 deletion src/col/vct/col/check/Check.scala
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ sealed trait CheckError {
"This dereference does not take place on one of the endpoints in the surrounding `seq_prog`."
)
case ChorStatement(s) =>
Seq(context(s) -> "This statement is not allowed in `seq_prog`.")
Seq(context(s) -> "This statement is not allowed in `choreography`.")
case SeqProgInstanceMethodArgs(m) =>
Seq(
context(m) ->
Expand Down
2 changes: 1 addition & 1 deletion src/rewrite/vct/rewrite/veymont/EncodeChoreography.scala
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,7 @@ case class EncodeChoreography[Pre <: Generation]()
"Ignoring endpoint expr annotation at " + expr.o.shortPositionText
)
dispatch(expr)
case (mode, ChorExpr(inner)) => dispatch(expr)
case (mode, ChorExpr(inner)) => dispatch(inner)
case (_, expr) => expr.rewriteDefault()
}
}
20 changes: 12 additions & 8 deletions src/rewrite/vct/rewrite/veymont/StratifyExpressions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -126,11 +126,16 @@ case class StratifyExpressions[Pre <: Generation]()
else
es
}
foldAny(e.t)(exprs.map(point).map {
case (Some(endpoint), expr) =>
EndpointExpr[Post](succ(endpoint), dispatch(expr))(expr.o)
case (None, expr) => dispatch(expr)
})(e.o)
foldAny(e.t)(
exprs.map {
case e: ChorExpr[Pre] => (None, e)
case expr => point(expr)
}.map {
case (Some(endpoint), expr) =>
EndpointExpr[Post](succ(endpoint), dispatch(expr))(expr.o)
case (None, expr) => dispatch(expr)
}
)(e.o)
}

// "Points" an expression in the direction of an endpoint if possible
Expand All @@ -141,9 +146,8 @@ case class StratifyExpressions[Pre <: Generation]()
(Some(endpoint), e)
case Seq() => (None, e)
case _ =>
throw MultipleEndpoints(
e
) // Expr uses multiple endpoints - for now we should disallow that.
// Expr uses multiple endpoints - for now we should disallow that.
throw MultipleEndpoints(e)
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -11,49 +11,46 @@ class TechnicalVeyMontExamplesSpec extends VercorsSpec {
// 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 "resolutionError:seqProgInvocation" flag
"--veymont-generate-permissions" example
s"$wd/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl")
// (vercors
// should verify
// using silicon flag "--veymont-generate-permissions"
// example s"$wd/checkMainSyntaxAndWellFormedness/IfCondition.pvl")

(vercors
should verify
using silicon flag "--veymont-generate-permissions"
example s"$wd/checkMainSyntaxAndWellFormedness/MainConstructorWithArgs.pvl")
(vercors should verify using silicon flag
"--veymont-generate-permissions" example
s"$wd/checkMainSyntaxAndWellFormedness/MainConstructorWithArgs.pvl")

// vercors should verify using silicon flag "--veymont-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:seqProgStatement"
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/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")

// TODO (RR): Re-enable once loop unanimity is re-implemented
// (vercors should fail withCode "loopUnanimityNotMaintained" using silicon flag
// "--veymont-generate-permissions" example
// s"$wd/checkMainSyntaxAndWellFormedness/WhileCondition.pvl")

// (vercors
// should error
Expand All @@ -65,8 +62,12 @@ class TechnicalVeyMontExamplesSpec extends VercorsSpec {
// flag "--veymont-generate-permissions"
// example s"$wd/checkMainSyntaxAndWellFormedness/WrongSyntax.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 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 flag "--veymont-generate-permissions" example s"$wd/various.pvl"
}
19 changes: 11 additions & 8 deletions test/main/vct/test/integration/examples/VeyMontExamplesSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,17 @@ import vct.test.integration.helper.VercorsSpec

class VeyMontExamplesSpec extends VercorsSpec {
val wd = "concepts/veymont/generatedPermissions"
vercors should verify using silicon flags "--veymont-generate-permissions" 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" 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"
// TODO (RR): Re-enable after stratified permissions are done
// 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"
// vercors should verify using silicon flags "--veymont-generate-permissions" example s"$wd/spectral-norm.pvl"
}
21 changes: 10 additions & 11 deletions test/main/vct/test/integration/helper/ExampleFiles.scala
Original file line number Diff line number Diff line change
Expand Up @@ -10,14 +10,11 @@ case object ExampleFiles {
"examples/archive/",
"examples/concepts/resourceValues",
"examples/technical/veymont",
"examples/concepts/veymont"
"examples/concepts/veymont",
"concepts/veymont/generatedPermissions",
).map(_.replaceAll("/", File.separator))

val IGNORE_EXTS: Seq[String] = Seq(
".h",
".bib",
".xml",
)
val IGNORE_EXTS: Seq[String] = Seq(".h", ".bib", ".xml")

val IGNORE_FILES: Set[String] = Set(
".gitignore",
Expand Down Expand Up @@ -45,9 +42,11 @@ case object ExampleFiles {
val FILES: Seq[Path] = find(Paths.get("examples"))

def find(directory: Path): Seq[Path] =
Files.list(directory)
.toScala(Seq)
.filterNot(f => EXCLUSIONS.exists(_(f)))
.sortBy(_.getFileName.toString)
.flatMap(f => if(Files.isDirectory(f)) find(f) else Seq(f))
Files.list(directory).toScala(Seq).filterNot(f => EXCLUSIONS.exists(_(f)))
.sortBy(_.getFileName.toString).flatMap(f =>
if (Files.isDirectory(f))
find(f)
else
Seq(f)
)
}

0 comments on commit 1d24a5e

Please sign in to comment.