diff --git a/Docs/docs/advanced/install-verification-backend.md b/Docs/docs/advanced/install-verification-backend.md new file mode 100644 index 0000000000..451ab038de --- /dev/null +++ b/Docs/docs/advanced/install-verification-backend.md @@ -0,0 +1,53 @@ +# Install Instructions for Amazon Linux + +## Get Java 11 +```sh +sudo rpm --import https://yum.corretto.aws/corretto.key +sudo curl -L-o /etc/yum.repos.d/corretto.repo https://yum.corretto.aws/corretto.repo +sudo yum install java-11-amazon-corretto-devel +``` + +## Get SBT +```sh +sudo rm -f /etc/yum.repos.d/bintray-rpm.repo || true +curl -L https://www.scala-sbt.org/sbt-rpm.repo > sbt-rpm.repo +sudo mv sbt-rpm.repo /etc/yum.repos.d/ +sudo yum install sbt +``` + +## Get Z3 +```sh +cd ~ +git clone https://github.com/Z3Prover/z3.git +cd z3 +python scripts/mk_make.py --java +cd build; make +``` +Then add `export PATH=$PATH:$HOME/z3/build/` and `export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$HOME/z3/build/` to your .zshrc and run +`source ~/.zshrc`. + +## Get UCLID5 +```sh +cd ~ +git clone https://github.com/uclid-org/uclid.git +cd uclid +sbt update clean compile "set fork:=true" test # should fail some tests that use cvc5 and delphi +sbt universal:packageBin +unzip target/universal/uclid-0.9.5.zip +``` +Then add `export PATH=$PATH:$HOME/uclid/uclid-0.9.5/bin/` to your .zshrc and run `source ~/.zshrc`. + +## Get PVerifier +```sh +cd ~ +git clone https://github.com/FedericoAureliano/P.git +cd P +# follow regular P install instructions +root=$(pwd) +cd $root/Bld +./build.sh +dotnet tool uninstall --global P +cd $root/Src/PCompiler/PCommandLine +dotnet pack PCommandLine.csproj --configuration Release --output ./publish -p:PackAsTool=true -p:ToolCommandName=P -p:Version=2.1.3 +dotnet tool install P --global --add-source ./publish +``` \ No newline at end of file diff --git a/Docs/docs/tutorial/advanced/twophasecommitverification.md b/Docs/docs/tutorial/advanced/twophasecommitverification.md new file mode 100644 index 0000000000..259b7b184e --- /dev/null +++ b/Docs/docs/tutorial/advanced/twophasecommitverification.md @@ -0,0 +1,388 @@ +# Introduction to Formal Verification in P + +This tutorial describes the formal verification features of P through an example. We assume that the reader has P installed along with the verification dependencies (i,e., UCLID5 and Z3). Installation instructions are available [here](https://github.com/p-org/P/blob/master/Docs/docs/advanced/install-verification-backend.md). + +When using P for formal verification, our goal is to show that no execution of any test driver will violate a specification. To do this, we will rely on proofs by induction---more on that later. This backend is different from P's explicit state model checker, which you are accustomed to using. These differences can influence the modeling decisions you make. + +To get a sense of these differences, and to cover the new features in P for verification, we will verify a simplified 2PC protocol. The P tutorial already describes a 2PC protocol, but we will make some different modeling choices that will make the verification process easier. In particular, we will follow the modeling decisions made by [Zhang et al.](https://www.usenix.org/system/files/osdi24-zhang-nuda.pdf) in their running example. + +## 2PC Model + +The 2PC protocol consists of two types of machines: coordinator and participant. There is a single coordinator, who receives requests from the outside world, and a set of participants, that must agree on whether to accept or reject the request. If any participant wants to reject the request, they must all agree to reject the request; if all participants want to accept the request, then they must all agree to accept the request. The job of the coordinator is to mediate this agreement. +To accomplish this, the system executes the following steps: + +1. The coordinator sends a message to all participants which asks the participants to vote on the request in question. +2. When a participant receives this vote request message, they reply with their vote. +3. When the coordinator receives a "no" vote---indicating that a participant wants to reject the request---it will send a message to all participants telling them to abort the request. +4. Otherwise, the coordinator tallies the "yes" vote. If all participants have voted "yes," then the coordinator sends a message to all participants telling them to commit the request. +5. When a participant receives either a commit or abort message from the coordinator, it store the decision locally. + +This system is extremely easy to model in P. Before defining the machines in the system, let's declare the five types of messages that are sent. + +``` +type tVoteResp = (source: machine); // we will keep track of who sent a vote +event eVoteReq; +event eYes: tVoteResp; +event eNo: tVoteResp; +event eAbort; +event eCommit; +``` + +### The Coordinator + +The coordinator is a machine with a single variable that we will use to keep track of votes. This machine has four states: one to kickoff the voting process, one to collect the votes; and two to indicate if the voting process resulted in a commit or an abort. + +``` +machine Coordinator +{ + var yesVotes: set[machine]; // set of machines that have voted yes + + start state Init {...} + state WaitForResponses {...} + state Committed {ignore eYes, eNo;} + state Aborted {ignore eYes, eNo;} +} +``` + +In the above code we omitted the internal details of states. Now let's go through these details one by one. First, the start state, called Init, contains a single for-loop that sends a vote request message to all the participants in the system. We use a function called "participants" to get the set of active participants. + +``` + start state Init { + entry { + var p: machine; + foreach (p in participants()) + { + send p, eVoteReq; // broadcast vote request to all participants + } + goto WaitForResponses; // move to WaitForResponses state + } + } +``` + +Second, the `WaitForResponses` state has two event handlers, one for each type of vote that participants can cast. + +``` +state WaitForResponses { + on eYes do (resp: tVoteResp) {...} + on eNo do (resp: tVoteResp) {...} +} +``` + +The details of when the coordinator receives "no" votes is simpler, so lets begin there. When the coordinator receives a "no" vote, it sends an abort message to all participants. + +``` +on eNo do (resp: tVoteResp) { + var p: machine; + foreach (p in participants()) + { + send p, eAbort; // broadcast abort to all participants + } + goto Aborted; +} +``` + +When a coordinator receives a "yes" vote, it will tally the vote and only broadcast a commit message to all participants if all participants have voted yes. + +``` +on eYes do (resp: tVoteResp) { + var p: machine; + yesVotes += (resp.source); + if (yesVotes == participants()) { // if everyone voted "yes" + foreach (p in participants()) + { + send p, eCommit; // broadcast commit message + } + goto Committed; // move to committed state: request was accepted + } +} +``` + +The final two states, `Committed` and `Aborted` will remain empty for now: we just want to use them to indicate the state of a request. + +### Participants + +Participants are slightly simpler. They consist of two states: one that does all the work, and two that we use to indicate that a request has been committed or aborted, just like we did for the coordinator. + +``` +machine Participant { + start state Undecided {...} + state Accepted {ignore eVoteReq, eCommit, eAbort;} + state Rejected {ignore eVoteReq, eCommit, eAbort;} +} +``` + +The main state, called "Undecided," has three event handlers: one for responding to vote requests, and two simpler ones for handling commit and abort messages. + +``` +on eVoteReq do { + // vote based on your preference! + if (preference(this)) { + send coordinator(), eYes, (source = this,); + } else { + send coordinator(), eNo, (source = this,); + } +} + +on eCommit do {goto Accepted;} +on eAbort do {goto Rejected;} +``` + +We use a function called "preference" to decide whether to vote yes or no on a transaction. We also use a function, "coordinator," to get the address of the coordinator machine. + +## Pure Functions + +The 2PC model described above uses three special functions, `participants`, `coordinator`, and `preference`, that capture the set of participants, the coordinator in charge, and the preference of individual participants for the given request. In this simple system, there is always one coordinator and a fixed set of participants, but we want the proof to work for any function that satisfies those conditions. In P, we can use the new concept of "pure" functions to model this (what SMT-LIB calls functions). Specifically, we can declare the three special functions as follows. + +``` +pure participants(): set[machine]; +pure coordinator(): machine; +pure preference(m: machine) : bool; +``` + +The participants function is a pure function with no body that takes no argument and returns a set of machines. The coordinator function is similar but only returns a single machine. The preference function, which also has no body, takes a machine and returns a preference. We call these functions "pure" because they can have no side-effects and behave like mathematical functions (e.g., calling the same pure function twice with the same arguments must give the same result). When pure functions do not have bodies, they are like foreign functions that we can guarantee don't have side-effects. When pure functions do have bodies, the bodies must be side-effect-free expressions. + +## Initialization Conditions + +We want our model to capture many different system configurations (e.g., number of participants) but not all configurations are valid. For example, we want to constrain the `participants` function to only point to participant machines. Initialization conditions let us constrain the kinds of systems that we consider. You can think of these as constraints that P test harnesses have to satisfy to be considered valid. + +In our 2PC model, for example, we can state that, at initialization, there is a unique machine of type coordinator, and the `coordinator` function points to that machine; and every machine in the participants set is a machine of type participant. + +``` +init-condition forall (m: machine) :: m == coordinator() == m is Coordinator; +init-condition forall (m: machine) :: m in participants() == m is Participant; +``` + +We can also state that all `yesVotes` tallies start empty. + +``` +init-condition forall (c: Coordinator) :: c.yesVotes == default(set[machine]); +``` + +When we write a proof of correctness later in this tutorial, we will be restricting the systems that we consider to those that satisfy the initialization conditions listed above. + +## Quantifiers and Machine Types + +Our initialization conditions contain two new P features: the `init` keyword, and quantified expressions (`forall` and `exists`). Even more interesting, one quantifier above is over a machine subtype (`coordinator`). + +In P, the only way to dereference a machine variable inside of a specification (like the `init-condition`s above) is by specifically quantifying over that machine type. In other words, `forall (c: Coordinator) :: c.yesVotes == default(set[machine])` is legal but `forall (c: machine) :: c.yesVotes == default(set[machine])` is not, even though they might appear to be similar. The reason for this is that selecting (using the `.` operator) on an incorrect subtype (e.g., trying to get `yesVotes` from a participant machine) is undefined. Undefined behavior in formal verification can lead to surprising results that can be really hard to debug, so in P we syntactically disallow this kind of undefined behavior altogether. + +## P's Builtin Specifications And Our First Proof Attempt + +Using the code described above, and by setting the target to `UCLID5` in the `.pproj` file, you can now run the verification engine for the first time (execute `p compile`). This run will result in a large list of failures, containing items like `āŒ Failed to verify that Coordinator never receives eVoteReq in Init`. These failures represent P's builtin requirements that all events are handled. They also give us a glimpse into how verification by induction works. + +Proofs by induction consist of a base case check and an inductive step check. The inductive step is more interesting and so we will focus our attention there. The high level idea is that you assume you are in a _good_ state of the system (I will describe what I mean by _good_ in the next section), and then you check if taking any step of the system will again land you in a _good_ state. in P, taking a step of the system means executing any event handler in any machine. + +When we ran our verification engine it reported that it failed to prove that all of P's builtin specifications were satisfied. Specifically, the verification engine gave us a list of all the builtin specifications that it failed to prove, like ``āŒ Failed to verify that Coordinator never receives eVoteReq in Init``. + +The verification engine is unable to prove these properties not because the system is incorrect, but rather because it needs help from the user to complete it's proof: it needs the user to define the _good_ states. More formally, it needs the user to define an inductive invariant that implies that no builtin P specification is violated. + +## Invariants And Our First Proof + +Users can provide invariants to P using the `invariant` keyword. The goal is to find a set of invariants whose conjunction is inductive and implies the desired property. For now, the desired property is that no builtin P specification is violated. + +In the 2PC model, the following 10 invariants are sufficient to prove that no builtin P specification is violated. + +``` +invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator; +invariant participant_set: forall (m: machine) :: m in participants() == m is Participant; + +invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; +invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; +invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; +invariant never_yes_to_participant: forall (e: event, p: Participant) :: e is eYes && e targets p ==> !inflight e; +invariant never_yes_to_init: forall (e: event, c: Coordinator) :: e is eYes && e targets c && c is Init ==> !inflight e; +invariant never_no_to_participant: forall (e: event, p: Participant) :: e is eNo && e targets p ==> !inflight e; +invariant never_no_to_init: forall (e: event, c: Coordinator) :: e is eNo && e targets c && c is Init ==> !inflight e; +invariant req_implies_not_init: forall (e: event, c: Coordinator) :: e is eVoteReq && c is Init ==> !inflight e; +``` + +The first two invariants state that, over the run of the system, our assumptions about the `coordinator` and `participants` functions remain satisfied. The next eight invariants ensure that messages target the correct kind of machine. For example, the invariant called `never_req_to_coordinator` says that there is never a vote request message going to a coordinator. These invariants use the special predicate `inflight` which is true iff the argument message has been sent but not received. P also supports a similar predicate called `sent` which is true iff the argument message has been sent. + +After adding these invariants, we can re-run the verification engine to get the following output. + +``` +šŸŽ‰ Verified 10 invariants! +āœ… one_coordinator +āœ… participant_set +āœ… never_commit_to_coordinator +āœ… never_abort_to_coordinator +āœ… never_req_to_coordinator +āœ… never_yes_to_participant +āœ… never_yes_to_init +āœ… never_no_to_participant +āœ… never_no_to_init +āœ… req_implies_not_init +āŒ Failed to verify 30 properties! +ā“ Failed to verify invariant never_commit_to_coordinator at PSrc/System.p:13:5 +... +ā“ Failed to verify invariant never_no_to_participant at PSrc/System.p:40:12 +``` + +What went wrong? Well, loops are tricky to reason about, so P requires users to provide loop invariants. You can think of these as summaries of what the loop does. P uses these summaries to prove other properties and checks that the loops actually abide by the given summaries. For example, we can add loop invariants to the first broadcast loop that we wrote---the one that sends out vote requests---as follows. + +``` +foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eVoteReq; +{ + send p, eVoteReq; +} +``` + +After adding similar loop invariants to all three loops in the model, we can re-run the verification engine to get the following output. + +``` +šŸŽ‰ Verified 10 invariants! +āœ… one_coordinator +āœ… participant_set +āœ… never_commit_to_coordinator +āœ… never_abort_to_coordinator +āœ… never_req_to_coordinator +āœ… never_yes_to_participant +āœ… never_yes_to_init +āœ… never_no_to_participant +āœ… never_no_to_init +āœ… req_implies_not_init +āœ… default P proof obligations +``` + +Notice that our initial model uses `ignore` statements that we did not describe when introducing the model. If we remove these statements, the verification engine will not be able to prove that no builtin P specification is violated. In some cases, that is because the ignore statements are necessary. For example, it is possible for the coordinator to receive a "yes" or "no" vote when it is in the `Aborted` state. The `ignore` keyword lets us tell the verifier that we have thought of these cases. + +## Invariant Groups, Proof Scripts, and Proof Caching + +When writing larger proofs, it will become useful to group invariants into lemmas, and then to tell the verifier how to use these lemmas for its proof checking. This helps the user organize their proofs; it helps the verifier construct smaller, more stable queries; and it helps avoid checking the same queries over and over, through caching. + +For example, we will write more complex specifications for the 2PC protocol but we will continue to verify that the builtin P specifications are satisfied. Instead of having to execute the verifier over and over to check these builtin properties as we build our larger proofs, we want to cache these results. Futhermore, we don't want any new specifications to interfere with these proof results---unless the model changes there really is no reason to look for a different proof of these same properties. + +P allows users to define invariant groups, like the following. + +``` +Lemma system_config { + invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator; + invariant participant_set: forall (m: machine) :: m in participants() == m is Participant; + invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; + invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; + invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; + invariant never_yes_to_participant: forall (e: event, p: Participant) :: e is eYes && e targets p ==> !inflight e; + invariant never_yes_to_init: forall (e: event, c: Coordinator) :: e is eYes && e targets c && c is Init ==> !inflight e; + invariant never_no_to_participant: forall (e: event, p: Participant) :: e is eNo && e targets p ==> !inflight e; + invariant never_no_to_init: forall (e: event, c: Coordinator) :: e is eNo && e targets c && c is Init ==> !inflight e; + invariant req_implies_not_init: forall (e: event, c: Coordinator) :: e is eVoteReq && c is Init ==> !inflight e; +} +``` + +These are all the same invariants we used above but now grouped inside a lemma called `system_config`. We can then use this lemma to decompose our proof using a proof script. + +``` +Proof { + prove system_config; + prove default using system_config; +} +``` + +This proof script has two steps. First it says that we need to prove that the lemma always holds (that the conjunction of the invariants are inductive for this model). Second we prove that P's default specifications always hold and tell the solver to use the `system_config` lemma to do so. When we run the verification engine again, we will get the following output. + +``` +šŸŽ‰ Verified 10 invariants! +āœ… system_config: one_coordinator +āœ… system_config: participant_set +āœ… system_config: never_commit_to_coordinator +āœ… system_config: never_abort_to_coordinator +āœ… system_config: never_req_to_coordinator +āœ… system_config: never_yes_to_participant +āœ… system_config: never_yes_to_init +āœ… system_config: never_no_to_participant +āœ… system_config: never_no_to_init +āœ… system_config: req_implies_not_init +āœ… default P proof obligations +``` + +Notice that the first time you run this verification it will take much longer than the second time. That is because the proof is cached and the solver is not executed the second time. If we don't change our model or our lemma, these queries will never be executed again. + +## First 2PC Specification and Proof + +Proving that the builtin P specifications are satisfied is all well and good, but it isn't exactly the most interesting property. Zhang et al. provide a more exciting specification that we can verify ("2PC-Safety"). Translated into P, their specification looks like the following invariant. + +``` +invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2)); +``` + +This invariant says that if any participant is in the accepted state, then every participant must have wanted to accept the request. Zhang et al. also provide a set of inductive invariants that help prove the safety property above (Fig. 5 in their paper). For our model in P, this set of invariants looks like the following. + +``` +Lemma kondo { + invariant a1a: forall (e: eYes) :: inflight e ==> e.source in participants(); + invariant a1b: forall (e: eNo) :: inflight e ==> e.source in participants(); + invariant a2a: forall (e: eYes) :: inflight e ==> preference(e.source); + invariant a2b: forall (e: eNo) :: inflight e ==> !preference(e.source); + invariant a3b: forall (e: eAbort) :: inflight e ==> coordinator() is Aborted; + invariant a3a: forall (e: eCommit) :: inflight e ==> coordinator() is Committed; + invariant a4: forall (p: Participant) :: p is Accepted ==> coordinator() is Committed; + invariant a5: forall (p: Participant, c: Coordinator) :: p in c.yesVotes ==> preference(p); + invariant a6: coordinator() is Committed ==> (forall (p: Participant) :: p in participants() ==> preference(p)); +} +``` + +Given the desired safety property that we want to prove and the set of invariants that helps us prove it, we can write the following proof script in P that checks that the proof by induction passes. + +``` +Proof { + prove system_config; + prove kondo using system_config; + prove safety using kondo; + prove default using system_config; +} +``` + +Running the verification engine on this file will produce the following. + +``` +šŸŽ‰ Verified 20 invariants! +āœ… safety +āœ… system_config: one_coordinator +āœ… system_config: participant_set +āœ… system_config: never_commit_to_coordinator +āœ… system_config: never_abort_to_coordinator +āœ… system_config: never_req_to_coordinator +āœ… system_config: never_yes_to_participant +āœ… system_config: never_yes_to_init +āœ… system_config: never_no_to_participant +āœ… system_config: never_no_to_init +āœ… system_config: req_implies_not_init +āœ… kondo: a1a +āœ… kondo: a1b +āœ… kondo: a2a +āœ… kondo: a2b +āœ… kondo: a3b +āœ… kondo: a3a +āœ… kondo: a4 +āœ… kondo: a5 +āœ… kondo: a6 +āœ… default P proof obligations +``` + +Showing that the verification passes. Notice that if you remove any of the invariants from the lemmas, like say `a5` in `kondo`, the proof will fail with the following output. + +``` +āŒ Failed to verify 1 properties! +ā“ Failed to verify invariant kondo: a6 at PSrc/System.p:27:12 +``` + +## Recap and Next Steps + +In this tutorial, we formally verified a simplified 2PC protocol in P. The full, final code for the verification is available [here](https://github.com/p-org/P/blob/experimental/pverifier/Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/PSrc/System.p). + +Our proof followed the running example of Zhang et al. but also included the verification of builtin P specifications. Along the way, we introduced the following new P keywords and concepts. + +1. `pure` functions; +2. `init-condition` predicates; +3. quantifiers; +4. proofs by induction; +5. `invariant`s; +6. `inflight` and `sent`; +6. loop invariants; +7. `lemma`s as invariant groups; +8. `proof` scripts; and +9. proof caching. + +In a future tutorial, we will expand on this simple 2PC protocol by introducing a key-value store and a monitor specification. \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs b/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs index 23c7968fb9..cb0178ce11 100644 --- a/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs +++ b/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs @@ -175,6 +175,10 @@ private void WriteTree(IPAST tree) WriteStmt("assert ", assertStmt.Assertion, ", \"", assertStmt.Message, "\";"); break; + case AssumeStmt assumeStmt: + WriteStmt("assume ", assumeStmt.Assumption, ", \"", assumeStmt.Message, "\";"); + break; + case AssignStmt assignStmt: WriteStmt(assignStmt.Location, " = ", assignStmt.Value, ";"); break; diff --git a/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs b/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs index 3de4fc381c..682f159229 100644 --- a/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs +++ b/Src/PCompiler/CompilerCore/Backend/IRTransformer.cs @@ -364,6 +364,22 @@ private List SimplifyStatement(IPStmt statement) }).ToList())); return assertDeps.Concat(new List{ifStmtForAssert}) .ToList(); + + case AssumeStmt assumeStmt: + (var assumeExpr, var assumeDeps) = SimplifyExpression(assumeStmt.Assumption); + (var amessageExpr, var amessageDeps) = SimplifyExpression(assumeStmt.Message); + if (assumeExpr is BoolLiteralExpr) + { + return assumeDeps.Concat(amessageDeps).Concat(new []{new AssumeStmt(location, assumeExpr, amessageExpr)}).ToList(); + } + + var aifStmtForAssert = new IfStmt(location, assumeExpr, new NoStmt(location), new CompoundStmt( + location, amessageDeps.Concat(new[] + { + new AssumeStmt(location, assumeExpr, amessageExpr) + }).ToList())); + return assumeDeps.Concat(new List{aifStmtForAssert}) + .ToList(); case AssignStmt assignStmt: (var assignLV, var assignLVDeps) = SimplifyLvalue(assignStmt.Location); @@ -434,7 +450,6 @@ private List SimplifyStatement(IPStmt statement) new CompoundStmt(ifStmt.ElseBranch.SourceLocation, elseBranch)) }) .ToList(); - case AddStmt addStmt: var (addVar, addVarDeps) = SimplifyLvalue(addStmt.Variable); var (addVal, addValDeps) = SimplifyArgPack(new[] { addStmt.Value }); diff --git a/Src/PCompiler/CompilerCore/Backend/PVerifier/CompilationContext.cs b/Src/PCompiler/CompilerCore/Backend/PVerifier/CompilationContext.cs new file mode 100644 index 0000000000..5d46170946 --- /dev/null +++ b/Src/PCompiler/CompilerCore/Backend/PVerifier/CompilationContext.cs @@ -0,0 +1,11 @@ +namespace Plang.Compiler.Backend.PVerifier; + +internal class CompilationContext : CompilationContextBase +{ + public CompilationContext(ICompilerConfiguration job) : base(job) + { + FileName = $"{ProjectName}.ucl"; + } + + public string FileName { get; set; } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs new file mode 100644 index 0000000000..4fcaae9a15 --- /dev/null +++ b/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs @@ -0,0 +1,2091 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using System.IO; +using System.Linq; +using System.Security.Cryptography; +using System.Text.RegularExpressions; +using System.Threading; +using LiteDB; +using Plang.Compiler.TypeChecker; +using Plang.Compiler.TypeChecker.AST; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.AST.Expressions; +using Plang.Compiler.TypeChecker.AST.Statements; +using Plang.Compiler.TypeChecker.AST.States; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.Backend.PVerifier; + +public class PVerifierCache +{ + public string Reply { get; set; } + public byte[] Checksum { get; set; } +} + +public class PVerifierCodeGenerator : ICodeGenerator +{ + private CompilationContext _ctx; + private CompiledFile _src; + private HashSet _optionsToDeclare; + private HashSet _chooseToDeclare; + private HashSet _setCheckersToDeclare; + private Dictionary> _specListenMap; // keep track of the procedure names for each event + private Dictionary _fileToProofCommands; + private Dictionary> _proofCommandToFiles; + private List _commands; + private Dictionary> _invariantDependencies; + private HashSet _provenInvariants; + private Scope _globalScope; + + public bool HasCompilationStage => true; + + public void Compile(ICompilerConfiguration job) + { + List undefs = []; + List fails = []; + List failMessages = []; + HashSet succeededInv = []; + HashSet failedInv = []; + var missingDefault = true; + + // Open database (or create if doesn't exist) + var db = new LiteDatabase(Path.Join(job.OutputDirectory.FullName, ".verifier-cache.db")); + var md5 = MD5.Create(); + // Get a collection (or create, if doesn't exist) + var qCollection = db.GetCollection("qCollection"); + + int parallelism = job.Parallelism; + if (parallelism == 0) + { + parallelism = Environment.ProcessorCount; + } + + foreach (var cmd in _commands) + { + if (cmd.Name.Contains("default")) + { + missingDefault = false; + } + job.Output.WriteInfo($"Proving: {cmd.Name}"); + Dictionary checklist = _proofCommandToFiles[cmd].ToDictionary(x => x, x => false); + Dictionary tasks = []; + + // prefill (check cache for everything, but only spin up `parallelism` number of runs + foreach (var f in checklist) + { + using (var stream = File.OpenRead(Path.Join(job.OutputDirectory.FullName, f.Key))) + { + var checksum = md5.ComputeHash(stream); + var hit = qCollection.FindOne(x => x.Checksum == checksum); + if (hit != null) + { + checklist[f.Key] = true; + var currUndefs = Regex.Matches(hit.Reply, @"UNDEF -> (.*), line (\d+)"); + var currFails = Regex.Matches(hit.Reply, @"FAILED -> (.*), line (\d+)"); + undefs.AddRange(currUndefs); + fails.AddRange(currFails); + var (invs, failed, msgs) = + AggregateResults(job, f.Key, currUndefs.ToList(), currFails.ToList()); + succeededInv.UnionWith(invs); + failedInv.UnionWith(failed); + failMessages.AddRange(msgs); + } + else if (tasks.Count < parallelism) + { + var args = new[] { "-M", f.Key }; + tasks.Add(f.Key, Compiler.NonBlockingRun(job.OutputDirectory.FullName, "uclid", args)); + } + } + } + + var numCompleted = checklist.Values.Sum(x => x ? 1 : 0); + Console.Write($"\ršŸ” Checked {numCompleted}/{checklist.Count} goals..."); + + // fetch + while (checklist.ContainsValue(false)) + { + Dictionary newTasks = []; + foreach (var r in tasks) + { + if (!r.Value.HasExited || checklist[r.Key]) continue; + // checklist is true if we've already done this + checklist[r.Key] = true; + + var exitCode = Compiler.WaitForResult(r.Value, out var stdout, out var stderr); + if (exitCode != 0) + { + throw new TranslationException($"Verifying generated UCLID5 code FAILED!\n" + $"{stdout}\n" + + $"{stderr}\n"); + } + + r.Value.Kill(); + + // add stdout to the database along with the corresponding checksum of the uclid query + using (var stream = File.OpenRead(Path.Join(job.OutputDirectory.FullName, r.Key))) + { + var newResult = new PVerifierCache + { + Reply = stdout, + Checksum = md5.ComputeHash(stream) + }; + qCollection.Insert(newResult); + } + + var currUndefs = Regex.Matches(stdout, @"UNDEF -> (.*), line (\d+)"); + var currFails = Regex.Matches(stdout, @"FAILED -> (.*), line (\d+)"); + undefs.AddRange(currUndefs); + fails.AddRange(currFails); + var (invs, failed, msgs) = AggregateResults(job, r.Key, currUndefs.ToList(), currFails.ToList()); + succeededInv.UnionWith(invs); + failedInv.UnionWith(failed); + failMessages.AddRange(msgs); + + // find someone that hasn't run and isn't running and run it + var newTask = checklist.FirstOrDefault(x => + x.Value == false && !tasks.ContainsKey(x.Key) && !newTasks.ContainsKey(x.Key)).Key; + if (newTask == null) continue; + var args = new[] { "-M", newTask }; + newTasks.Add(newTask, Compiler.NonBlockingRun(job.OutputDirectory.FullName, "uclid", args)); + } + + if (newTasks.Count == 0) + { + Thread.Sleep(500); + } + else + { + newTasks.ToList().ForEach(x => tasks.Add(x.Key, x.Value)); + } + + numCompleted = checklist.Values.Sum(x => x ? 1 : 0); + Console.Write($"\ršŸ” Checked {numCompleted}/{checklist.Count} goals..."); + } + + Console.WriteLine(); + } + + succeededInv.ExceptWith(failedInv); + job.Output.WriteInfo($"\nšŸŽ‰ Verified {succeededInv.Count} invariants!"); + foreach (var inv in succeededInv) + { + job.Output.WriteInfo($"āœ… {inv.Name.Replace("_PGROUP_", ": ")}"); + } + if (!missingDefault && failMessages.Count == 0) + { + job.Output.WriteInfo($"āœ… default P proof obligations"); + } + + MarkProvenInvariants(succeededInv); + ShowRemainings(job, failedInv, missingDefault); + if (failMessages.Count > 0) + { + job.Output.WriteInfo($"āŒ Failed to verify {failMessages.Count} properties!"); + foreach (var msg in failMessages) + { + job.Output.WriteError(msg); + } + } + + db.Dispose(); + md5.Dispose(); + } + + private void MarkProvenInvariants(HashSet succeededInv) + { + foreach (var inv in _invariantDependencies.Keys) + { + _invariantDependencies[inv].ExceptWith(succeededInv); + } + + foreach (var inv in _invariantDependencies.Keys) + { + if (succeededInv.Contains(inv)) + { + _provenInvariants.Add(inv); + } + } + } + + private void ShowRemainings(ICompilerConfiguration job, HashSet failedInv, bool missingDefault) + { + HashSet remaining = []; + foreach (var inv in _provenInvariants) + { + foreach (var dep in _invariantDependencies[inv]) + { + if (!failedInv.Contains(dep) && !_provenInvariants.Contains(dep)) + { + remaining.Add(dep); + } + } + } + + if (remaining.Count > 0 || missingDefault) + { + job.Output.WriteWarning("ā“ Remaining Goals:"); + foreach (var inv in remaining) + { + job.Output.WriteWarning($"- {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(inv)}"); + } + + if (missingDefault) + { + job.Output.WriteWarning($"- default P proof obligations"); + } + } + } + + private void ProcessFailureMessages(List collection, string[] query, string reason, List failedInv, + List failMessages) + { + foreach (Match match in collection) + { + foreach (var feedback in match.Groups[1].Captures.Zip(match.Groups[2].Captures)) + { + var line = query[int.Parse(feedback.Second.ToString()) - 1]; + var step = feedback.First.ToString().Contains("[Step #0]") ? "(base case)" : ""; + var matchName = Regex.Match(line, @"// Failed to verify invariant (.*) at (.*)"); + var invName = matchName.Groups[1].Value.Replace("_PGROUP_", ": "); + failedInv.Add(invName); + failMessages.Add($"{reason} {line.Split("//").Last()} {step}"); + } + } + } + + // returns invariants that were successfully verified and failure messages + private (HashSet, HashSet, List) AggregateResults(ICompilerConfiguration job, + string filename, List undefs, List fails) + { + var cmd = _fileToProofCommands[filename]; + var query = File.ReadLines(job.OutputDirectory.FullName + "/" + filename).ToArray(); + List failedInv = []; + List failMessages = []; + ProcessFailureMessages(fails, query, "āŒ", failedInv, failMessages); + ProcessFailureMessages(undefs, query, "ā“", failedInv, failMessages); + if (failedInv.Count == 0) + { + return ([.. cmd.Goals], [], []); + } + + HashSet succeededInv = []; + foreach (var inv in cmd.Goals) + { + if (!failedInv.Contains(inv.Name)) + { + succeededInv.Add(inv); + } + } + + return (succeededInv, failedInv.Select(x => + { + _globalScope.Get(x, out Invariant i); + return i; + }).ToHashSet(), failMessages); + } + + public IEnumerable GenerateCode(ICompilerConfiguration job, Scope globalScope) + { + _ctx = new CompilationContext(job); + _optionsToDeclare = []; + _chooseToDeclare = []; + _specListenMap = new Dictionary>(); + _setCheckersToDeclare = []; + _fileToProofCommands = []; + _invariantDependencies = []; + _provenInvariants = []; + _proofCommandToFiles = []; + _commands = []; + _globalScope = globalScope; + BuildDependencies(globalScope); + var filenamePrefix = $"{job.ProjectName}_"; + List files = []; + if (!globalScope.ProofCommands.Any()) + { + var proof = new ProofCommand("default", null) + { + Goals = globalScope.AllDecls.OfType().ToList(), + Premises = [] + }; + _commands.Add(proof); + _proofCommandToFiles.Add(proof, []); + files.AddRange(CompileToFile($"{filenamePrefix}default", proof, true, true, false)); + } + else + { + foreach (var proofCmd in globalScope.ProofCommands) + { + if (proofCmd.Goals.Count == 1 && proofCmd.Goals[0].IsDefault) + { + proofCmd.Name = "default" + proofCmd.Name; + proofCmd.Goals = []; + _commands.Add(proofCmd); + _proofCommandToFiles.Add(proofCmd, []); + files.AddRange(CompileToFile($"{filenamePrefix}default", proofCmd, true, true, true)); + } + else + { + _proofCommandToFiles.Add(proofCmd, []); + files.AddRange(CompileToFile($"{filenamePrefix}{proofCmd.Name.Replace(",", "_").Replace(" ", "_")}", proofCmd, true, false, false)); + _commands.Add(proofCmd); + } + } + } + + return files; + } + + private CompiledFile GenerateCompiledFile(ProofCommand cmd, string name, Machine m, State s, Event e) + { + string filename; + if (e == null) + { + filename = $"{name}_{m.Name}_{s.Name}.ucl"; + } + else + { + filename = $"{name}_{m.Name}_{s.Name}_{e.Name}.ucl"; + } + + var file = new CompiledFile(filename); + _fileToProofCommands.Add(filename, cmd); + _proofCommandToFiles[cmd].Add(filename); + return file; + } + + private List CompileToFile(string name, ProofCommand cmd, bool sanityCheck, bool handlerCheck, bool builtin) + { + var machines = (from m in _globalScope.AllDecls.OfType() where !m.IsSpec select m).ToList(); + var events = _globalScope.AllDecls.OfType().ToList(); + List files = []; + foreach (var m in machines) + { + if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(m.Name)) + { + foreach (var s in m.States) + { + if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(s.Name)) + { + _src = GenerateCompiledFile(cmd, name, m, s, null); + files.Add(_src); + GenerateMain(m, s, null, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck, builtin); + } + + foreach (var e in events.Where(e => !e.IsNullEvent && !e.IsHaltEvent && s.HasHandler(e))) + { + if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(e.Name)) + { + _src = GenerateCompiledFile(cmd, name, m, s, e); + files.Add(_src); + GenerateMain(m, s, e, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck, builtin); + } + } + } + } + } + + Console.WriteLine($"Generated {files.Count} files for {name}"); + return files; + } + + private void BuildDependencies(Scope globalScope) + { + foreach (var cmd in globalScope.ProofCommands) + { + foreach (var goal in cmd.Goals) + { + foreach (var dep in cmd.Premises) + { + if (goal == dep) continue; + if (!_invariantDependencies.ContainsKey(goal)) + { + _invariantDependencies.Add(goal, []); + } + + _invariantDependencies[goal].Add(dep); + } + } + } + } + + private string ShowInvariant(IPExpr e) + { + if (e is InvariantRefExpr inv) return inv.Invariant.Name; + else return e.SourceLocation.GetText(); + } + + private void EmitLine(string str) + { + _ctx.WriteLine(_src.Stream, str); + } + + // Prefixes to avoid name clashes and keywords + private static string BuiltinPrefix => "P_"; + private static string UserPrefix => "User_"; + private static string EventPrefix => "Event_"; + private static string GotoPrefix => "PGoto_"; + private static string MachinePrefix => "PMachine_"; + private static string LocalPrefix => "PLocal_"; + private static string OptionPrefix => "POption_"; + private static string ChoosePrefix => "PChoose_"; + private static string CheckerPrefix => "PChecklist_"; + private static string SpecPrefix => "PSpec_"; + private static string InvariantPrefix => "PInv_"; + + // P values that don't have a direct UCLID5 equivalent + private static string PNull => $"{BuiltinPrefix}Null"; + private static string PNullDeclaration => $"type {PNull} = enum {{{PNull}}};"; + + private static string DefaultMachineRef => $"{BuiltinPrefix}DefaultMachine"; + private static string DefaultMachineDeclaration => $"const {DefaultMachineRef}: {MachineRefT};"; + + // P types that don't have a direct UCLID5 equivalent + private static string StringT => $"{BuiltinPrefix}String"; + private static string StringTDeclaration => $"type {StringT};"; + private static string DefaultString => $"{BuiltinPrefix}DefaultString"; + private static string DefaultStringDeclaration => $"const {DefaultString}: {StringT};"; + + /******************************** + * type StateADT = record {sent: [LabelADT]boolean, received: [LabelADT]boolean, machines: [MachineRefT]MachineStateADT}; + * var state: StateT; + *******************************/ + private static string StateAdt => $"{BuiltinPrefix}StateAdt"; + private static string StateAdtSentSelector => $"{StateAdt}_Sent"; + private static string StateAdtReceivedSelector => $"{StateAdt}_Received"; + private static string StateAdtMachinesSelector => $"{StateAdt}_Machines"; + + private static string StateAdtConstruct(string sent, string received, string machines) + { + return + $"const_record({StateAdtSentSelector} := {sent}, {StateAdtReceivedSelector} := {received}, {StateAdtMachinesSelector} := {machines})"; + } + + private static string StateAdtSelectSent(string state) + { + return $"{state}.{StateAdtSentSelector}"; + } + + private static string StateAdtSelectReceived(string state) + { + return $"{state}.{StateAdtReceivedSelector}"; + } + + private static string StateAdtSelectMachines(string state) + { + return $"{state}.{StateAdtMachinesSelector}"; + } + + private static string StateAdtDeclaration() + { + return + $"type {StateAdt} = record {{{StateAdtSentSelector}: [{LabelAdt}]boolean, {StateAdtReceivedSelector}: [{LabelAdt}]boolean, {StateAdtMachinesSelector}: [{MachineRefT}]{MachineStateAdt}}};"; + } + + private static string InFlight(string state, string action) + { + return $"({StateAdtSelectSent(state)}[{action}] && !{StateAdtSelectReceived(state)}[{action}])"; + } + + private static string StateVar => $"{BuiltinPrefix}State"; + private static string StateVarDeclaration => $"var {StateVar}: {StateAdt};"; + + private static string Deref(string r) + { + return $"{StateAdtSelectMachines(StateVar)}[{r}]"; + } + + /******************************** + * type MachineRef; + * + * type MachineStateADT = record {stage: boolean; machine: MachineADT}; + * + * // where Mi are the declared machines, Si their P state names, and MiFjl their fields + * type MachineADT = | M0(M0_State: S0, M0F00, ..., M0F0n) + * | ... + * | Mk(Mk_State: Sk, MkFk0, ..., MkFkm) + *******************************/ + private static string MachineRefT => $"{MachinePrefix}Ref_t"; + private static string MachineRefTDeclaration => $"type {MachineRefT};"; + private static string MachineStateAdt => $"{MachinePrefix}State_ADT"; + private static string MachineStateAdtStageSelector => $"{MachineStateAdt}_Stage"; + private static string MachineStateAdtMachineSelector => $"{MachineStateAdt}_Machine"; + + private static string MachineStateAdtConstruct(string stage, string machine) + { + return + $"const_record({MachineStateAdtStageSelector} := {stage}, {MachineStateAdtMachineSelector} := {machine})"; + } + + private static string MachineStateAdtSelectStage(string state) + { + return $"{state}.{MachineStateAdtStageSelector}"; + } + + private static string MachineStateAdtSelectMachine(string state) + { + return $"{state}.{MachineStateAdtMachineSelector}"; + } + + private static string MachineStateAdtDeclaration() + { + return + $"type {MachineStateAdt} = record {{{MachineStateAdtStageSelector}: boolean, {MachineStateAdtMachineSelector}: {MachineAdt}}};"; + } + + private static string MachineAdt => $"{MachinePrefix}ADT"; + + private string MachineAdtDeclaration(List machines) + { + var sum = string.Join("\n\t\t| ", machines.Select(ProcessMachine)); + return $"datatype {MachineAdt} = \n\t\t| {sum};"; + + string ProcessMachine(Machine m) + { + var fields = string.Join(", ", + m.Fields.Select(f => $"{MachinePrefix}{m.Name}_{f.Name}: {TypeToString(f.Type)}")); + if (m.Fields.Any()) fields = ", " + fields; + + return $"{MachinePrefix}{m.Name} ({MachinePrefix}{m.Name}_State: {MachinePrefix}{m.Name}_StateAdt{fields})"; + } + } + + private static string MachineAdtConstructM(Machine m, List args) + { + return $"{MachinePrefix}{m.Name}({string.Join(", ", args)})"; + } + + private static string MachineAdtSelectState(string instance, Machine m) + { + return $"{instance}.{MachinePrefix}{m.Name}_State"; + } + + private static string MachineStateAdtSelectState(string state, Machine m) + { + return MachineAdtSelectState(MachineStateAdtSelectMachine(state), m); + } + + private static string MachineAdtSelectField(string instance, Machine m, Variable f) + { + return $"{instance}.{MachinePrefix}{m.Name}_{f.Name}"; + } + + private static string MachineStateAdtSelectField(string state, Machine m, Variable f) + { + return MachineAdtSelectField(MachineStateAdtSelectMachine(state), m, f); + } + + private static string MachinePStateDeclaration(Machine m) + { + var states = string.Join(", ", m.States.Select(s => $"{MachinePrefix}{m.Name}_{s.Name}")); + return $"type {MachinePrefix}{m.Name}_StateAdt = enum {{{states}}};"; + } + + private static string MachineAdtIsM(string instance, Machine machine) + { + return $"is_{MachinePrefix}{machine.Name}({instance})"; + } + + private static string MachineStateAdtIsM(string state, Machine machine) + { + return $"is_{MachinePrefix}{machine.Name}({MachineStateAdtSelectMachine(state)})"; + } + + private static string MachineStateAdtInS(string state, Machine m, State s) + { + return + $"({MachineStateAdtIsM(state, m)} && {MachineStateAdtSelectState(state, m)} == {MachinePrefix}{m.Name}_{s.Name})"; + } + + + private static string InStartPredicateDeclaration(List machines) + { + var input = $"{LocalPrefix}state"; + var cases = machines.Select(ProcessMachine).ToList(); + var body = cases.Aggregate("false", (acc, pair) => $"if ({pair.Item1}) then ({pair.Item2})\n\t\telse ({acc})"); + return $"define {BuiltinPrefix}InStart({input}: {MachineStateAdt}) : boolean =\n\t\t{body};"; + + (string, string) ProcessMachine(Machine m) + { + var machine = $"{MachineStateAdtSelectMachine(input)}"; + var state = $"{machine}.{MachinePrefix}{m.Name}_State"; + var start = $"{MachinePrefix}{m.Name}_{m.StartState.Name}"; + var check = $"{state} == {start}"; + var guard = MachineAdtIsM(machine, m); + return (guard, check); + } + } + + private static string InEntryPredicateDeclaration() + { + var input = $"{LocalPrefix}state"; + return + $"define {BuiltinPrefix}InEntry({input}: {MachineStateAdt}) : boolean = {MachineStateAdtSelectStage(input)};"; + } + + /******************************** + * type LabelAdt = record {target: MachineRef, action: EitherEventOrGotoAdt} + * + * datatype EitherEventOrGotoAdt = | EventLabel (event: EventAdt) + * | GotoLabel (goto: GotoAdt) + * + * // where Ei is an event, Pi is the payload of the event and Ti is the type of the payload + * datatype EventAdt = | E0 (P0: T0) + * | ... + * | En (Pn: Tn) + * + * // where Si are as in MachineAdt and A0 are the arguments to the entry handler of the state + * datatype GotoAdt = | M0 (M0_State: S0, A0: T0) + * | ... + * | Mn (Mn_State: Sn, An: Tn) + *******************************/ + private static string LabelAdt => $"{BuiltinPrefix}Label"; + private static string LabelAdtTargetSelector => $"{LabelAdt}_Target"; + private static string LabelAdtActionSelector => $"{LabelAdt}_Action"; + private static string LabelAdtActionCountSelector => $"{LabelAdt}_ActionCount"; + + private static string LabelAdtDeclaration() + { + return + $"type {LabelAdt} = record {{{LabelAdtTargetSelector}: {MachineRefT}, {LabelAdtActionSelector}: {EventOrGotoAdt}, {LabelAdtActionCountSelector}: integer}};"; + } + + private void IncrementActionCount() + { + EmitLine($"{BuiltinPrefix}ActionCount = {BuiltinPrefix}ActionCount + 1;"); + } + + private static string LabelAdtConstruct(string target, string action) + { + return + $"const_record({LabelAdtTargetSelector} := {target}, {LabelAdtActionSelector} := {action}, {LabelAdtActionCountSelector} := {BuiltinPrefix}ActionCount)"; + } + + private static string LabelAdtSelectTarget(string label) + { + return $"{label}.{LabelAdtTargetSelector}"; + } + + private static string LabelAdtSelectAction(string label) + { + return $"{label}.{LabelAdtActionSelector}"; + } + + private static string LabelAdtSelectActionCount(string label) + { + return $"{label}.{LabelAdtActionCountSelector}"; + } + + + private static string EventOrGotoAdt => $"{BuiltinPrefix}EventOrGoto"; + private static string EventOrGotoAdtEventConstructor => $"{EventOrGotoAdt}_Event"; + private static string EventOrGotoAdtGotoConstructor => $"{EventOrGotoAdt}_Goto"; + private static string EventOrGotoAdtEventSelector => $"{EventOrGotoAdt}_Event_Event"; + private static string EventOrGotoAdtGotoSelector => $"{EventOrGotoAdt}_Goto_Goto"; + + private static string EventOrGotoAdtDeclaration() + { + var e = $"| {EventOrGotoAdtEventConstructor}({EventOrGotoAdtEventSelector}: {EventAdt})"; + var g = $"| {EventOrGotoAdtGotoConstructor}({EventOrGotoAdtGotoSelector}: {GotoAdt})"; + return $"datatype {EventOrGotoAdt} = \n\t\t{e}\n\t\t{g};"; + } + + private static string EventOrGotoAdtConstructEvent(string e) + { + return $"{EventOrGotoAdtEventConstructor}({e})"; + } + + private string EventOrGotoAdtConstructEvent(Event ev, IPExpr arg) + { + var payload = arg is null ? "" : ExprToString(arg); + var e = EventAdtConstruct(payload, ev); + return $"{EventOrGotoAdtEventConstructor}({e})"; + } + + + private static string EventOrGotoAdtConstructGoto(string g) + { + return $"{EventOrGotoAdtGotoConstructor}({g})"; + } + + private string EventOrGotoAdtConstructGoto(State state, IPExpr payload) + { + var g = GotoAdtConstruct(state, payload); + return $"{EventOrGotoAdtGotoConstructor}({g})"; + } + + private static string EventOrGotoAdtSelectEvent(string eventOrGoto) + { + return $"{eventOrGoto}.{EventOrGotoAdtEventSelector}"; + } + + private static string EventOrGotoAdtSelectGoto(string eventOrGoto) + { + return $"{eventOrGoto}.{EventOrGotoAdtGotoSelector}"; + } + + private static string EventOrGotoAdtIsEvent(string eventOrGoto) + { + return $"is_{EventOrGotoAdtEventConstructor}({eventOrGoto})"; + } + + private static string EventOrGotoAdtIsGoto(string eventOrGoto) + { + return $"is_{EventOrGotoAdtGotoConstructor}({eventOrGoto})"; + } + + private static string EventAdt => $"{EventPrefix}Adt"; + + private string EventAdtDeclaration(List events) + { + var declarationSum = string.Join("\n\t\t| ", events.Select(EventDeclarationCase)); + return $"datatype {EventAdt} = \n\t\t| {declarationSum};"; + + string EventDeclarationCase(Event e) + { + var pt = e.PayloadType.IsSameTypeAs(PrimitiveType.Null) + ? "" + : $"{EventPrefix}{e.Name}_Payload: {TypeToString(e.PayloadType)}"; + return + $"{EventPrefix}{e.Name} ({pt})"; + } + } + + private static string EventAdtSelectPayload(string eadt, Event e) + { + return $"{eadt}.{EventPrefix}{e.Name}_Payload"; + } + + private static string EventAdtConstruct(string payload, Event e) + { + return $"{EventPrefix}{e.Name}({payload})"; + } + + private static string EventAdtIsE(string instance, Event e) + { + return $"is_{EventPrefix}{e.Name}({instance})"; + } + + private static string EventOrGotoAdtIsE(string instance, Event e) + { + var isEvent = EventOrGotoAdtIsEvent(instance); + var selectEvent = EventOrGotoAdtSelectEvent(instance); + var correctEvent = EventAdtIsE(selectEvent, e); + return $"({isEvent} && {correctEvent})"; + } + + private static string LabelAdtIsE(string instance, Event e) + { + var action = LabelAdtSelectAction(instance); + return EventOrGotoAdtIsE(action, e); + } + + private static string LabelAdtSelectPayloadField(string instance, Event e, NamedTupleEntry field) + { + var action = LabelAdtSelectAction(instance); + return $"{EventAdtSelectPayload(EventOrGotoAdtSelectEvent(action), e)}.{field.Name}"; + } + + private static string GotoAdt => $"{GotoPrefix}Adt"; + + private string GotoAdtDeclaration(IEnumerable machines) + { + List<(State, Variable)> gotos = []; + foreach (var m in machines) + foreach (var s in m.States) + { + var f = s.Entry; + // get the arguments to the entry handler + Variable a = null; + if (f is not null && s.Entry.Signature.Parameters.Count > 0) + { + a = s.Entry.Signature.Parameters[0]; + } + + gotos.Add((s, a)); + } + + var sum = string.Join("\n\t\t| ", gotos.Select(ProcessGoto)); + + return $"datatype {GotoAdt} = \n\t\t| {sum};"; + + string ProcessGoto((State, Variable) g) + { + var prefix = $"{GotoPrefix}{g.Item1.OwningMachine.Name}_{g.Item1.Name}"; + if (g.Item2 is null) + { + return prefix + "()"; + } + + return prefix + $"({prefix}_{g.Item2.Name}: {TypeToString(g.Item2.Type)})"; + } + } + + private string GotoAdtConstruct(State s, IPExpr p) + { + var payload = p is null ? "" : ExprToString(p); + return $"{GotoPrefix}{s.OwningMachine.Name}_{s.Name}({payload})"; + } + + private string GotoAdtSelectParam(string instance, string param, State s) + { + return $"{instance}.{GotoPrefix}{s.OwningMachine.Name}_{s.Name}_{param}"; + } + + private static string GotoAdtIsS(string instance, State s) + { + return $"is_{GotoPrefix}{s.OwningMachine.Name}_{s.Name}({instance})"; + } + + private static string EventOrGotoAdtIsS(string instance, State s) + { + var isGoto = EventOrGotoAdtIsGoto(instance); + var selectGoto = EventOrGotoAdtSelectGoto(instance); + var correctGoto = GotoAdtIsS(selectGoto, s); + return $"({isGoto} && {correctGoto})"; + } + + private static string LabelAdtIsS(string instance, State s) + { + var action = LabelAdtSelectAction(instance); + return EventOrGotoAdtIsS(action, s); + } + + + /******************************** + * Spec machines are treated differently than regular machines. For example, there is only ever a single instance of + * each spec machine. + * + * To handle spec machines, + * 1) we create a global variable for each of their fields; + * 2) keep track of what events the spec machines are listening to and the corresponding handleers; + * 3) create a procedure per spec machine handler that operates on the variables from (1); and + * 4) whenever a regular machine sends an event, we call the appropriate handler from (2). + *******************************/ + private void SpecVariableDeclarations(List specs) + { + foreach (var spec in specs) + { + EmitLine( + $"type {SpecPrefix}{spec.Name}_StateAdt = enum {{{string.Join(", ", spec.States.Select(n => $"{SpecPrefix}{spec.Name}_{n.Name}"))}}};"); + EmitLine($"var {SpecPrefix}{spec.Name}_State: {SpecPrefix}{spec.Name}_StateAdt;"); + foreach (var f in spec.Fields) + { + EmitLine($"var {SpecPrefix}{spec.Name}_{f.Name}: {TypeToString(f.Type)};"); + } + } + } + + private void GenerateSpecProcedures(List specs, List goals, bool generateSanityChecks = false) + { + foreach (var spec in specs) + { + foreach (var f in spec.Methods) + { + var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}"); + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + EmitLine($"procedure [inline] {name}({string.Join(", ", ps)})"); + if (!f.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null)) + { + EmitLine($"\treturns ({BuiltinPrefix}Return: {TypeToString(f.Signature.ReturnType)})"); + } + + EmitLine("{"); + + // declare local variables corresponding to the global spec variables + EmitLine($"var {LocalPrefix}state: {SpecPrefix}{spec.Name}_StateAdt;"); + EmitLine($"var {LocalPrefix}sent: [{LabelAdt}]boolean;"); + foreach (var v in spec.Fields) + { + EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + } + + // declare local variables for the method + foreach (var v in f.LocalVariables) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + // foreach (var v in f.LocalVariables) EmitLine($"{GetLocalName(v)} = {DefaultValue(v.Type)};"); + + // Set the local variables corresponding to the global spec variables to the correct starting value + EmitLine($"{LocalPrefix}sent = {StateAdtSelectSent(StateVar)};"); + foreach (var v in spec.Fields) + EmitLine($"{GetLocalName(v)} = {SpecPrefix}{spec.Name}_{v.Name};"); + + GenerateStmt(f.Body, spec, goals, generateSanityChecks); + + // update the global variables + EmitLine($"{SpecPrefix}{spec.Name}_State = {LocalPrefix}state;"); + foreach (var v in spec.Fields) + { + EmitLine($"{SpecPrefix}{spec.Name}_{v.Name} = {GetLocalName(v)};"); + } + + EmitLine("}\n"); + } + } + } + + private void GenerateSpecHandlers(List specs) + { + foreach (var spec in specs) + { + var events = spec.Observes.Events; + foreach (var e in events) + { + var procedureName = $"{SpecPrefix}{spec.Name}_{e.Name}"; + if (_specListenMap.ContainsKey(e)) + { + _specListenMap[e].Add(procedureName); + } + else + { + _specListenMap.Add(e, [procedureName]); + } + + EmitLine($"procedure [inline] {procedureName}({SpecPrefix}Payload: {TypeToString(e.PayloadType)})"); + EmitLine("{"); + EmitLine("case"); + foreach (var state in spec.States) + { + var handlers = state.AllEventHandlers.ToDictionary(); + if (state.HasHandler(e)) + { + var handler = handlers[e]; + var precondition = $"{SpecPrefix}{spec.Name}_State == {SpecPrefix}{spec.Name}_{state.Name}"; + EmitLine($"({precondition}) : {{"); + switch (handler) + { + case EventDoAction eventDoAction: + var f = eventDoAction.Target; + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + var payload = f.Signature.Parameters.Count > 0 ? $"{SpecPrefix}Payload" : ""; + EmitLine($"call {name}({payload});"); + break; + default: + throw new NotSupportedException( + $"Not supported handler ({handler}) at {GetLocation(handler)}"); + } + + EmitLine("}"); + } + } + + EmitLine("esac"); + EmitLine("}"); + } + } + } + + /******************************** + * Traverse the P AST and generate the UCLID5 code using the types and helpers defined above + *******************************/ + private void + GenerateMain(Machine machine, State state, Event @event, List goals, + List requires, bool generateSanityChecks, bool handlerCheck, bool builtin) + { + if (builtin) + { + goals = requires; + } + + EmitLine("module main {"); + + var machines = (from m in _globalScope.AllDecls.OfType() where !m.IsSpec select m).ToList(); + var specs = (from m in _globalScope.AllDecls.OfType() where m.IsSpec select m).ToList(); + var events = _globalScope.AllDecls.OfType().ToList(); + // goals = _globalScope.AllDecls.OfType().ToList(); + var axioms = _globalScope.AllDecls.OfType().ToList(); + var pures = _globalScope.AllDecls.OfType().ToList(); + + EmitLine(PNullDeclaration); + EmitLine(DefaultMachineDeclaration); + EmitLine(StringTDeclaration); + EmitLine(DefaultStringDeclaration); + EmitLine(""); + + GenerateUserEnums(_globalScope.AllDecls.OfType()); + GenerateUserTypes(_globalScope.AllDecls.OfType()); + EmitLine(""); + + EmitLine(EventAdtDeclaration(events)); + EmitLine(""); + EmitLine(GotoAdtDeclaration(machines)); + EmitLine(""); + EmitLine(EventOrGotoAdtDeclaration()); + EmitLine(LabelAdtDeclaration()); + EmitLine($"var {BuiltinPrefix}ActionCount: integer;"); + EmitLine(""); + + EmitLine(MachineRefTDeclaration); + foreach (var m in machines) + { + EmitLine(MachinePStateDeclaration(m)); + } + + EmitLine(MachineAdtDeclaration(machines)); + EmitLine(MachineStateAdtDeclaration()); + EmitLine(""); + + EmitLine(StateAdtDeclaration()); + EmitLine(StateVarDeclaration); + EmitLine(""); + + SpecVariableDeclarations(specs); + EmitLine(""); + + EmitLine(InStartPredicateDeclaration(machines)); + EmitLine(InEntryPredicateDeclaration()); + EmitLine(""); + + GenerateInitBlock(machines, specs, _globalScope.AllDecls.OfType()); + EmitLine(""); + + // pick a random label and handle it (with some guards to make sure we always handle gotos before events) + if (_ctx.Job.HandlesAll) + { + GenerateNextBlock(machines, events, handlerCheck); + EmitLine(""); + } + + // global functions + GenerateGlobalProcedures(_globalScope.AllDecls.OfType(), goals, generateSanityChecks); + + // Spec support + GenerateSpecProcedures(specs, goals, generateSanityChecks); // generate spec methods, called by spec handlers + GenerateSpecHandlers(specs); // will populate _specListenMap, which is used when ever there is a send statement + EmitLine(""); + + // non-handler functions for handlers + GenerateMachineProcedures(machine, goals, + generateSanityChecks); // generate machine methods, called by handlers below + EmitLine(""); + + // generate the handlers + if (@event != null) + { + GenerateEventHandler(state, @event, goals, requires, generateSanityChecks); + } + else + { + GenerateEntryHandler(state, goals, requires, generateSanityChecks); + } + + EmitLine(""); + + // These have to be done at the end because we don't know what we need until we generate the rest of the code + GenerateOptionTypes(); + EmitLine(""); + GenerateCheckerVars(); + EmitLine(""); + GenerateChooseProcedures(); + EmitLine(""); + + foreach (var pure in pures) + { + var args = string.Join(", ", + pure.Signature.Parameters.Select(p => $"{LocalPrefix}{p.Name}: {TypeToString(p.Type)}")); + if (pure.Body is null) + { + EmitLine($"function {pure.Name}({args}): {TypeToString(pure.Signature.ReturnType)};"); + } + else + { + EmitLine( + $"define {pure.Name}({args}): {TypeToString(pure.Signature.ReturnType)} = {ExprToString(pure.Body)};"); + } + } + + EmitLine(""); + + if (!builtin) + { + foreach (var inv in requires) + { + EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};"); + } + } + + foreach (var inv in goals) + { + EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};"); + EmitLine( + $"invariant _{InvariantPrefix}{inv.Name}: {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} globally"); + } + + EmitLine(""); + + foreach (var ax in axioms) + { + EmitLine($"axiom {ExprToString(ax.Body)};"); + } + + EmitLine(""); + + if (generateSanityChecks) + { + // invariants to ensure unique action IDs + EmitLine( + $"define {InvariantPrefix}Unique_Actions(): boolean = forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {StateAdtSelectSent(StateVar)}[a1] && {StateAdtSelectSent(StateVar)}[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};"); + EmitLine($"invariant _{InvariantPrefix}Unique_Actions: {InvariantPrefix}Unique_Actions();"); + EmitLine( + $"define {InvariantPrefix}Increasing_Action_Count(): boolean = forall (a: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;"); + EmitLine( + $"invariant _{InvariantPrefix}Increasing_Action_Count: {InvariantPrefix}Increasing_Action_Count();"); + // invariants to ensure received is a subset of sent + EmitLine( + $"define {InvariantPrefix}Received_Subset_Sent(): boolean = forall (a: {LabelAdt}) :: {StateAdtSelectReceived(StateVar)}[a] ==> {StateAdtSelectSent(StateVar)}[a];"); + EmitLine($"invariant _{InvariantPrefix}Received_Subset_Sent: {InvariantPrefix}Received_Subset_Sent();"); + EmitLine(""); + } + + GenerateControlBlock(machine, state, @event); + + // close the main module + EmitLine("}"); + } + + private void GenerateUserEnums(IEnumerable enums) + { + foreach (var e in enums) + { + var variants = string.Join(", ", e.Values.Select(v => UserPrefix + v.Name)); + EmitLine($"type {UserPrefix}{e.Name} = enum {{{variants}}};"); + } + } + + private void GenerateUserTypes(IEnumerable types) + { + foreach (var t in types) EmitLine($"type {UserPrefix}{t.Name} = {TypeToString(t.Type)};"); + } + + private void GenerateInitBlock(List machines, List specs, IEnumerable starts) + { + var state = Deref("r"); + EmitLine("init {"); + EmitLine("// Every machine begins in their start state"); + EmitLine($"assume(forall (r: {MachineRefT}) :: {BuiltinPrefix}InStart({state}));"); + EmitLine("// Every machine begins with their entry flag set"); + EmitLine($"assume(forall (r: {MachineRefT}) :: {BuiltinPrefix}InEntry({state}));"); + EmitLine("// The buffer starts completely empty"); + EmitLine($"{StateAdtSelectSent(StateVar)} = const(false, [{LabelAdt}]boolean);"); + EmitLine($"{StateAdtSelectReceived(StateVar)} = const(false, [{LabelAdt}]boolean);"); + + EmitLine("// User assumptions"); + foreach (var assumes in starts) + { + EmitLine($"assume ({ExprToString(assumes.Body)}); // {assumes.Name}"); + } + + // close the init block + EmitLine("}"); + } + + private void GenerateNextBlock(List machines, List events, bool handlerCheck) + { + var currentLabel = $"{BuiltinPrefix}CurrentLabel"; + // pick a random label and handle it + EmitLine("next {"); + EmitLine($"var {currentLabel}: {LabelAdt};"); + EmitLine($"if ({InFlight(StateVar, currentLabel)}) {{"); + EmitLine("case"); + foreach (var m in machines) + { + foreach (var s in m.States) + { + foreach (var e in events.Where(e => !e.IsNullEvent && !e.IsHaltEvent)) + { + if (!s.HasHandler(e)) + { + if (handlerCheck) + { + if (_ctx.Job.CheckOnly is null || _ctx.Job.CheckOnly == m.Name || + _ctx.Job.CheckOnly == s.Name || _ctx.Job.CheckOnly == e.Name) + { + EmitLine($"({EventGuard(m, s, e)}) : {{"); + EmitLine( + $"assert false; // Failed to verify that {m.Name} never receives {e.Name} in {s.Name}"); + EmitLine("}"); + } + } + } + } + } + } + + EmitLine("esac"); + EmitLine("}"); + // close the next block + EmitLine("}"); + return; + + string EventGuard(Machine m, State s, Event e) + { + var correctMachine = MachineStateAdtIsM(Deref(LabelAdtSelectTarget(currentLabel)), m); + var correctState = MachineStateAdtInS(Deref(LabelAdtSelectTarget(currentLabel)), m, s); + var correctEvent = LabelAdtIsE(currentLabel, e); + return string.Join(" && ", [correctMachine, correctState, correctEvent]); + } + } + + private void GenerateGlobalProcedures(IEnumerable functions, List goals, + bool generateSanityChecks = false) + { + // TODO: these should be side-effect free and we should enforce that + foreach (var f in functions) + { + var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}").Prepend($"this: {MachineRefT}"); + + if (f.Body is null) + { + EmitLine($"procedure [noinline] {f.Name}({string.Join(", ", ps)})"); + } + else + { + EmitLine($"procedure [inline] {f.Name}({string.Join(", ", ps)})"); + } + + if (!f.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null)) + { + var retName = f.ReturnVariable is null + ? $"{BuiltinPrefix}Return" + : $"{LocalPrefix}{f.ReturnVariable.Name}"; + EmitLine($"\treturns ({retName}: {TypeToString(f.Signature.ReturnType)})"); + } + + var i = 0; + foreach (var req in f.Requires) + { + i += 1; + EmitLine($"requires {ExprToString(req)}; // Violated precondition #{i} of {f.Name}"); + } + + foreach (var ensure in f.Ensures) + { + EmitLine($"ensures {ExprToString(ensure)};"); + } + + EmitLine("{"); + // declare local variables for the method + foreach (var v in f.LocalVariables) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + GenerateStmt(f.Body, null, goals, generateSanityChecks); + EmitLine("}\n"); + } + } + + private void GenerateMachineProcedures(Machine m, List goals, bool generateSanityChecks = false) + { + foreach (var f in m.Methods) + { + var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}") + .Prepend($"this: {MachineRefT}"); + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + EmitLine($"procedure [inline] {name}({string.Join(", ", ps)})"); + + var currState = Deref("this"); + + if (!f.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null)) + { + EmitLine($"\treturns ({BuiltinPrefix}Return: {TypeToString(f.Signature.ReturnType)})"); + } + + EmitLine("{"); + + // declare necessary local variables + EmitLine($"var {LocalPrefix}state: {MachinePrefix}{m.Name}_StateAdt;"); + EmitLine($"var {LocalPrefix}stage: boolean;"); + EmitLine($"var {LocalPrefix}sent: [{LabelAdt}]boolean;"); + foreach (var v in m.Fields) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + foreach (var v in f.LocalVariables) EmitLine($"var {GetLocalName(v)}: {TypeToString(v.Type)};"); + + // initialize all the local variables to the correct values + EmitLine($"{LocalPrefix}state = {MachineStateAdtSelectState(currState, m)};"); + EmitLine($"{LocalPrefix}stage = false;"); // this can be set to true by a goto statement + EmitLine($"{LocalPrefix}sent = {StateAdtSelectSent(StateVar)};"); + foreach (var v in m.Fields) + EmitLine($"{GetLocalName(v)} = {MachineStateAdtSelectField(currState, m, v)};"); + // foreach (var v in f.LocalVariables) EmitLine($"{GetLocalName(v)} = {DefaultValue(v.Type)};"); + + GenerateStmt(f.Body, null, goals, generateSanityChecks); + + var fields = m.Fields.Select(GetLocalName).Prepend($"{LocalPrefix}state").ToList(); + + // make a new machine + var newMachine = MachineAdtConstructM(m, fields); + // make a new machine state + var newMachineState = MachineStateAdtConstruct($"{LocalPrefix}stage", newMachine); + // update the machine map + EmitLine( + $"{StateAdtSelectMachines(StateVar)} = {StateAdtSelectMachines(StateVar)}[this -> {newMachineState}];"); + // update the buffer + EmitLine($"{StateAdtSelectSent(StateVar)} = {LocalPrefix}sent;"); + + EmitLine("}\n"); + } + } + + private void GenerateEntryHandler(State s, List goals, List requires, + bool generateSanityChecks = false) + { + var label = $"{LocalPrefix}Label"; + var target = LabelAdtSelectTarget(label); + var targetMachineState = Deref(target); + var action = LabelAdtSelectAction(label); + var g = EventOrGotoAdtSelectGoto(action); + var received = StateAdtSelectReceived(StateVar); + + EmitLine($"procedure [noinline] {s.OwningMachine.Name}_{s.Name}({label}: {LabelAdt})"); + EmitLine($"\trequires {InFlight(StateVar, label)};"); + EmitLine($"\trequires {EventOrGotoAdtIsGoto(action)};"); + EmitLine($"\trequires {GotoAdtIsS(g, s)};"); + EmitLine($"\trequires {MachineStateAdtInS(targetMachineState, s.OwningMachine, s)};"); + if (generateSanityChecks) + { + EmitLine($"\trequires {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tensures {InvariantPrefix}Unique_Actions();"); + EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();"); + EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent();"); + } + + foreach (var reqs in requires) + { + EmitLine($"\trequires {InvariantPrefix}{reqs.Name}();"); + } + + foreach (var inv in goals) + { + EmitLine($"\trequires {InvariantPrefix}{inv.Name}();"); + EmitLine( + $"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(s)}"); + } + + EmitLine("{"); + + if (s.Entry is null) + { + EmitLine($"var {LocalPrefix}stage: boolean;"); + EmitLine($"var {LocalPrefix}state: {MachinePrefix}{s.OwningMachine.Name}_StateAdt;"); + EmitLine($"var {LocalPrefix}received: [{LabelAdt}]boolean;"); + + EmitLine($"{LocalPrefix}stage = false;"); + EmitLine($"{LocalPrefix}state = {MachineStateAdtSelectState(targetMachineState, s.OwningMachine)};"); + EmitLine($"{received} = {received}[{label} -> true];"); + EmitLine($"{LocalPrefix}received = {received};"); + + var fields = s.OwningMachine.Fields + .Select(v => MachineStateAdtSelectField(targetMachineState, s.OwningMachine, v)) + .Prepend($"{LocalPrefix}state").ToList(); + // make a new machine + var newMachine = MachineAdtConstructM(s.OwningMachine, fields); + // make a new machine state + var newMachineState = MachineStateAdtConstruct($"{LocalPrefix}stage", newMachine); + // update the machine map + EmitLine( + $"{StateAdtSelectMachines(StateVar)} = {StateAdtSelectMachines(StateVar)}[{target} -> {newMachineState}];"); + // update the buffer + EmitLine($"{received} = {LocalPrefix}received;"); + } + else + { + var f = s.Entry; + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + var payload = f.Signature.Parameters.Count > 0 + ? $", {GotoAdtSelectParam(g, f.Signature.Parameters[0].Name, s)}" + : ""; + EmitLine($"{received} = {received}[{label} -> true];"); + EmitLine($"call {name}({target}{payload});"); + } + + EmitLine("}\n"); + } + + + private void GenerateEventHandler(State s, Event ev, List goals, List requires, + bool generateSanityChecks = false) + { + var label = $"{LocalPrefix}Label"; + EmitLine($"procedure [noinline] {s.OwningMachine.Name}_{s.Name}_{ev.Name}({label}: {LabelAdt})"); + + var target = LabelAdtSelectTarget(label); + var targetMachineState = Deref(target); + var action = LabelAdtSelectAction(label); + var e = EventOrGotoAdtSelectEvent(action); + var received = StateAdtSelectReceived(StateVar); + + EmitLine($"\trequires {InFlight(StateVar, label)};"); + EmitLine($"\trequires {MachineStateAdtInS(targetMachineState, s.OwningMachine, s)};"); + EmitLine($"\trequires {EventOrGotoAdtIsEvent(action)};"); + EmitLine($"\trequires {EventAdtIsE(e, ev)};"); + if (generateSanityChecks) + { + EmitLine($"\trequires {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tensures {InvariantPrefix}Unique_Actions();"); + EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();"); + EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent();"); + } + + var handler = s.AllEventHandlers.ToDictionary()[ev]; + + foreach (var reqs in requires) + { + EmitLine($"\trequires {InvariantPrefix}{reqs.Name}();"); + } + + foreach (var inv in goals) + { + EmitLine($"\trequires {InvariantPrefix}{inv.Name}();"); + EmitLine( + $"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(handler)}"); + } + + switch (handler) + { + case EventDefer _: + EmitLine("{"); + EmitLine("}\n"); + return; + case EventDoAction eventDoAction: + var f = eventDoAction.Target; + var line = _ctx.LocationResolver.GetLocation(f.SourceLocation).Line; + var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name; + var payload = f.Signature.Parameters.Count > 0 ? $", {EventAdtSelectPayload(e, ev)}" : ""; + EmitLine("{"); + EmitLine($"{received} = {received}[{label} -> true];"); + EmitLine($"call {name}({target}{payload});"); + EmitLine("}\n"); + return; + case EventIgnore _: + EmitLine("{"); + EmitLine("}\n"); + return; + default: + throw new NotSupportedException($"Not supported handler ({handler}) at {GetLocation(handler)}"); + } + } + + + private void GenerateControlBlock(Machine m, State s, Event e) + { + EmitLine("control {"); + EmitLine($"set_solver_option(\":Timeout\", {_ctx.Job.Timeout});"); // timeout per query in seconds + + EmitLine("induction(1);"); + + if (e == null) + { + EmitLine($"verify({m.Name}_{s.Name});"); + } + else + { + EmitLine($"verify({m.Name}_{s.Name}_{e.Name});"); + } + + EmitLine("check;"); + EmitLine("print_results;"); + EmitLine("}"); + } + + private string DefaultValue(PLanguageType ty) + { + return ty switch + { + EnumType enumType => UserPrefix + enumType.EnumDecl.Values.First().Name, + MapType mapType => + $"const({GetOptionName(mapType.ValueType)}_None(), {TypeToString(mapType)})", + NamedTupleType ntt => + $"const_record({string.Join(", ", ntt.Fields.Select(f => $"{f.Name} := {DefaultValue(f.Type)}"))})", + PermissionType _ => DefaultMachineRef, + PrimitiveType pt when pt.Equals(PrimitiveType.Bool) => "false", + PrimitiveType pt when pt.Equals(PrimitiveType.Int) => "0", + PrimitiveType pt when pt.Equals(PrimitiveType.String) => DefaultString, + PrimitiveType pt when pt.Equals(PrimitiveType.Machine) => DefaultMachineRef, + SetType setType => $"const(false, {TypeToString(setType)})", + TypeDefType tdType => DefaultValue(tdType.TypeDefDecl.Type), + _ => throw new NotSupportedException($"Not supported default: {ty} ({ty.OriginalRepresentation})"), + }; + } + + private void GenerateOptionTypes() + { + foreach (var ptype in _optionsToDeclare) + { + var opt = GetOptionName(ptype); + EmitLine($"datatype {opt} = "); + EmitLine($"\t| {opt}_Some ({opt}_Some_Value: {TypeToString(ptype)})"); + EmitLine($"\t| {opt}_None ();"); + } + } + + private void GenerateChooseProcedures() + { + foreach (var choosePt in _chooseToDeclare) + { + var proc = GetChooseName(choosePt); + EmitLine($"procedure [noinline] {proc}(inp: {TypeToString(choosePt)})"); + switch (choosePt) + { + case MapType mapType: + EmitLine($"\treturns (outp: {TypeToString(mapType.KeyType)})"); + EmitLine($"\tensures {OptionIsSome(mapType.ValueType, "inp[outp]")};"); + break; + case SetType setType: + EmitLine($"\treturns (outp: {TypeToString(setType.ElementType)})"); + EmitLine($"\tensures inp[outp];"); + break; + case PrimitiveType pt when pt.Equals(PrimitiveType.Int): + EmitLine($"\treturns (outp: {TypeToString(pt)})"); + EmitLine($"\tensures 0 <= outp && outp <= inp;"); + break; + default: + throw new NotSupportedException( + $"Not supported choose type: {choosePt} ({choosePt.OriginalRepresentation})"); + } + + EmitLine("{"); + EmitLine("}\n"); + } + } + + private string OptionConstructSome(PLanguageType t, string value) + { + return $"{GetOptionName(t)}_Some({value})"; + } + + private string OptionConstructNone(PLanguageType t) + { + return $"{GetOptionName(t)}_None()"; + } + + private string OptionIsSome(PLanguageType t, string instance) + { + return $"is_{GetOptionName(t)}_Some({instance})"; + } + + private string OptionIsNone(PLanguageType t, string instance) + { + return $"is_{GetOptionName(t)}_None({instance})"; + } + + private string OptionSelectValue(PLanguageType t, string instance) + { + return $"{instance}.{GetOptionName(t)}_Some_Value"; + } + + private void GenerateCheckerVars() + { + foreach (var ptype in _setCheckersToDeclare) + { + var name = GetCheckerName(ptype); + EmitLine($"var {name}: {TypeToString(ptype)};"); + } + } + + // specMachine is null iff we are not generating a statement for a spec machine + private void GenerateStmt(IPStmt stmt, Machine specMachine, List goals, + bool generateSanityChecks = false) + { + switch (stmt) + { + case CompoundStmt cstmt: + foreach (var s in cstmt.Statements) GenerateStmt(s, specMachine, goals, generateSanityChecks); + return; + case AssignStmt { Value: FunCallExpr, Location: VariableAccessExpr } cstmt: + var call = cstmt.Value as FunCallExpr; + var avax = cstmt.Location as VariableAccessExpr; + if (call == null) return; + var v = ExprToString(avax); + var f = call.Function.Name; + var fargs = call.Arguments.Select(ExprToString); + if (call.Function.Owner is not null) + { + fargs = fargs.Prepend("this"); + } + + EmitLine($"call ({v}) = {f}({string.Join(", ", fargs.Prepend("this"))});"); + return; + case AssignStmt { Value: ChooseExpr, Location: VariableAccessExpr } cstmt: + var chooseExpr = (ChooseExpr)cstmt.Value; + _chooseToDeclare.Add(chooseExpr.SubExpr.Type); + var cvax = (VariableAccessExpr)cstmt.Location; + var cv = ExprToString(cvax); + var cf = GetChooseName(chooseExpr.SubExpr.Type); + var arg = ExprToString(chooseExpr.SubExpr); + EmitLine($"call ({cv}) = {cf}({arg});"); + return; + case AssignStmt astmt: + switch (astmt.Location) + { + case VariableAccessExpr vax: + EmitLine($"{ExprToString(vax)} = {ExprToString(astmt.Value)};"); + return; + case MapAccessExpr { MapExpr: VariableAccessExpr } max: + var map = ExprToString(max.MapExpr); + var index = ExprToString(max.IndexExpr); + var t = ((MapType)max.MapExpr.Type).ValueType; + EmitLine($"{map} = {map}[{index} -> {OptionConstructSome(t, ExprToString(astmt.Value))}];"); + return; + case NamedTupleAccessExpr { SubExpr: VariableAccessExpr } tax: + var subExpr = ExprToString(tax.SubExpr); + var entry = tax.Entry.Name; + var field = tax.FieldName; + var fields = ((NamedTupleType)((TypeDefType)tax.SubExpr.Type).TypeDefDecl.Type).Fields; + var rhs = ExprToString(astmt.Value); + var build = string.Join(", ", + fields.Select( + f => f.Name == entry ? $"{entry} := {rhs}" : $"{f.Name} := {subExpr}.{f.Name}")); + EmitLine($"{subExpr} = const_record({build});"); + return; + } + + throw new NotSupportedException( + $"Not supported assignment expression: {astmt.Location} = {astmt.Value} ({GetLocation(astmt)})"); + case IfStmt ifstmt: + var cond = (ifstmt.Condition) switch + { + NondetExpr => "*", + _ => ExprToString(ifstmt.Condition), + }; + EmitLine($"if ({cond}) {{"); + GenerateStmt(ifstmt.ThenBranch, specMachine, goals, generateSanityChecks); + EmitLine("} else {"); + GenerateStmt(ifstmt.ElseBranch, specMachine, goals, generateSanityChecks); + EmitLine("}"); + return; + case AssertStmt astmt: + EmitLine($"// {((StringExpr)astmt.Message).BaseString}"); + EmitLine( + $"assert({ExprToString(astmt.Assertion)}); // Failed to verify assertion at {GetLocation(astmt)}"); + return; + case AssumeStmt astmt: + EmitLine($"// {((StringExpr)astmt.Message).BaseString}"); + EmitLine($"assume({ExprToString(astmt.Assumption)});"); + return; + case PrintStmt { Message: StringExpr } pstmt: + EmitLine($"// {((StringExpr)pstmt.Message).BaseString}"); + return; + case FunCallStmt fapp: + EmitLine( + $"call {fapp.Function.Name}({string.Join(", ", fapp.ArgsList.Select(ExprToString).Prepend("this"))});"); + return; + case AddStmt { Variable: VariableAccessExpr } astmt: + // v += (y) + var aset = ExprToString(astmt.Variable); + var akey = ExprToString(astmt.Value); + EmitLine($"{aset} = {aset}[{akey} -> true];"); + return; + case AddStmt { Variable: MapAccessExpr } astmt + when ((MapAccessExpr)astmt.Variable).MapExpr is VariableAccessExpr: + // m[x] += (y) + // m = m[x -> some((m[x].some)[y -> true])] + var mapInP = ((MapAccessExpr)astmt.Variable); + var mapTypeInP = (MapType)mapInP.MapExpr.Type; + var mapM = ExprToString(mapInP.MapExpr); + var locX = ExprToString(mapInP.IndexExpr); + var valY = ExprToString(astmt.Value); + var someMx = OptionSelectValue(mapTypeInP.ValueType, $"{mapM}[{locX}]"); + var someUpdated = OptionConstructSome(mapTypeInP.ValueType, $"{someMx}[{valY} -> true]"); + EmitLine($"{mapM} = {mapM}[{locX} -> {someUpdated}];"); + return; + case RemoveStmt { Variable: VariableAccessExpr } rstmt: + var rset = ExprToString(rstmt.Variable); + var rkey = ExprToString(rstmt.Value); + + switch (rstmt.Variable.Type) + { + case MapType mapType: + EmitLine($"{rset} = {rset}[{rkey} -> {OptionConstructNone(mapType.ValueType)}];"); + return; + case SetType _: + EmitLine($"{rset} = {rset}[{rkey} -> false];"); + return; + default: + throw new NotSupportedException( + $"Only support remove statements for sets and maps, got {rstmt.Variable.Type}"); + } + case InsertStmt { Variable: VariableAccessExpr } istmt: + var imap = ExprToString(istmt.Variable); + var idx = ExprToString(istmt.Index); + var value = OptionConstructSome(istmt.Value.Type, ExprToString(istmt.Value)); + EmitLine($"{imap} = {imap}[{idx} -> {value}];"); + return; + case ForeachStmt fstmt: + + switch (fstmt.IterCollection) + { + case KeysExpr keysExpr: + fstmt = new ForeachStmt(fstmt.SourceLocation, fstmt.Item, keysExpr.Expr, fstmt.Body, + fstmt.Invariants); + break; + } + + var item = GetLocalName(fstmt.Item); + var checker = GetCheckerName(fstmt.IterCollection.Type); + var collection = ExprToString(fstmt.IterCollection); + + switch (fstmt.IterCollection.Type) + { + case SetType setType: + // set the checker to default + EmitLine($"{checker} = {DefaultValue(setType)};"); + // remember to declare it later + _setCheckersToDeclare.Add(setType); + // havoc the item + EmitLine($"havoc {item};"); + EmitLine($"while ({checker} != {collection})"); + foreach (var inv in goals) + { + EmitLine( + $"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}"); + } + + if (generateSanityChecks) + { + EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tinvariant {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent();"); + // ensure uniqueness for the new ones too + EmitLine( + $"\tinvariant forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {LocalPrefix}sent[a1] && {LocalPrefix}sent[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};"); + EmitLine( + $"\tinvariant forall (a: {LabelAdt}) :: {LocalPrefix}sent[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;"); + + // ensure we only ever add sends + EmitLine( + $"\tinvariant forall (e: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[e] ==> {LocalPrefix}sent[e];"); + } + + // user given invariants + foreach (var inv in fstmt.Invariants) + { + EmitLine( + $"\tinvariant {ExprToString(inv)}; // Failed to verify loop invariant at {GetLocation(inv)}"); + } + + EmitLine("{"); + // assume that the item is in the set but hasn't been visited + EmitLine($"if ({collection}[{item}] && !{checker}[{item}]) {{"); + // the body of the loop + GenerateStmt(fstmt.Body, specMachine, goals, generateSanityChecks); + // update the checker + EmitLine($"{checker} = {checker}[{item} -> true];"); + EmitLine("}"); + // havoc the item + EmitLine($"havoc {item};"); + EmitLine("}"); + return; + case MapType mapType: + // set the checker to default + EmitLine($"{checker} = {DefaultValue(mapType)};"); + // remember to declare it later + _setCheckersToDeclare.Add(mapType); + // havoc the item, in this case it is a key + EmitLine($"havoc {item};"); + EmitLine($"while ({checker} != {collection})"); + foreach (var inv in goals) + { + EmitLine( + $"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}"); + } + + EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions();"); + EmitLine($"\tinvariant {InvariantPrefix}Increasing_Action_Count();"); + EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent();"); + // ensure uniqueness for the new ones too + EmitLine( + $"\tinvariant forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {LocalPrefix}sent[a1] && {LocalPrefix}sent[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};"); + EmitLine( + $"\tinvariant forall (a: {LabelAdt}) :: {LocalPrefix}sent[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;"); + + // ensure we only ever add sends + EmitLine( + $"\tinvariant forall (e: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[e] ==> {LocalPrefix}sent[e];"); + + // user given invariants + foreach (var inv in fstmt.Invariants) + { + EmitLine( + $"\tinvariant {ExprToString(inv)}; // Failed to verify loop invariant at {GetLocation(inv)}"); + } + + EmitLine("{"); + // assume that the item is in the set but hasn't been visited + EmitLine( + $"if ({OptionIsSome(mapType.ValueType, $"{collection}[{item}]")} && {OptionIsNone(mapType.ValueType, $"{checker}[{item}]")}) {{"); + // the body of the loop + GenerateStmt(fstmt.Body, specMachine, goals, generateSanityChecks); + // update the checker + EmitLine($"{checker} = {checker}[{item} -> {collection}[{item}]];"); + EmitLine("}"); + // havoc the item + EmitLine($"havoc {item};"); + EmitLine("}"); + return; + default: + throw new NotSupportedException( + $"Foreach over non-sets is not supported yet: {fstmt} ({GetLocation(fstmt)}"); + } + case GotoStmt gstmt when specMachine is null: + var gaction = EventOrGotoAdtConstructGoto(gstmt.State, gstmt.Payload); + var glabel = LabelAdtConstruct("this", gaction); + var glabels = StateAdtSelectSent(StateVar); + var newState = $"{MachinePrefix}{gstmt.State.OwningMachine.Name}_{gstmt.State.Name}"; + EmitLine($"{glabels} = {glabels}[{glabel} -> true];"); + IncrementActionCount(); + EmitLine($"{LocalPrefix}state = {newState};"); + EmitLine($"{LocalPrefix}stage = true;"); + return; + case GotoStmt gstmts: // when specMachine is not null + EmitLine($"{LocalPrefix}state = {SpecPrefix}{specMachine.Name}_{gstmts.State.Name};"); + EmitLine($"{LocalPrefix}stage = true;"); + return; + case SendStmt sstmt when specMachine is null: + if (sstmt.Arguments.Count > 1) + { + throw new NotSupportedException("We only support at most one argument to a send"); + } + + var ev = ((EventRefExpr)sstmt.Evt).Value; + var saction = EventOrGotoAdtConstructEvent(ev, sstmt.Arguments.Any() ? sstmt.Arguments.First() : null); + var slabel = LabelAdtConstruct(ExprToString(sstmt.MachineExpr), saction); + var slabels = $"{LocalPrefix}sent"; + EmitLine($"{slabels} = {slabels}[{slabel} -> true];"); + IncrementActionCount(); + foreach (var procedureName in _specListenMap.GetValueOrDefault(ev, [])) + { + var argument = sstmt.Arguments.Count > 0 ? $"{ExprToString(sstmt.Arguments[0])}" : PNull; + EmitLine($"call {procedureName}({argument});"); + } + + return; + case ReturnStmt rstmt: + EmitLine($"{BuiltinPrefix}Return = {ExprToString(rstmt.ReturnValue)};"); + return; + case null: + return; + } + + throw new NotSupportedException($"Not supported statement: {stmt} ({GetLocation(stmt)})"); + } + + private string ExprToString(IPExpr expr) + { + return expr switch + { + NamedTupleAccessExpr ntax => $"{ExprToString(ntax.SubExpr)}.{ntax.FieldName}", + VariableAccessExpr vax => GetLocalName(vax.Variable), + IntLiteralExpr i => i.Value.ToString(), + BoolLiteralExpr b => b.Value.ToString().ToLower(), + BinOpExpr bexpr => + $"({ExprToString(bexpr.Lhs)} {BinOpToString(bexpr.Operation)} {ExprToString(bexpr.Rhs)})", + UnaryOpExpr uexpr => $"({UnaryOpToString(uexpr.Operation)} {ExprToString(uexpr.SubExpr)})", + ThisRefExpr => "this", + EnumElemRefExpr e => $"{UserPrefix}{e.Value.Name}", + NamedTupleExpr t => NamedTupleExprHelper(t), + StringExpr s => + $"\"{s.BaseString}\" {(s.Args.Count != 0 ? "%" : "")} {string.Join(", ", s.Args.Select(ExprToString))}", + MapAccessExpr maex => + OptionSelectValue(((MapType)maex.MapExpr.Type).ValueType, + $"{ExprToString(maex.MapExpr)}[{ExprToString(maex.IndexExpr)}]"), + ContainsExpr cexp when cexp.Collection.Type.Canonicalize() is MapType => OptionIsSome( + ((MapType)cexp.Collection.Type).ValueType, + $"{ExprToString(cexp.Collection)}[{ExprToString(cexp.Item)}]"), + ContainsExpr cexp when cexp.Collection.Type.Canonicalize() is SetType => + $"{ExprToString(cexp.Collection)}[{ExprToString(cexp.Item)}]", + DefaultExpr dexp => DefaultValue(dexp.Type), + QuantExpr { Quant: QuantType.Forall } qexpr => + $"(forall ({BoundVars(qexpr.Bound)}) :: {Guard(qexpr.Bound, qexpr.Difference, true)}({ExprToString(qexpr.Body)}))", + QuantExpr { Quant: QuantType.Exists } qexpr => + $"(exists ({BoundVars(qexpr.Bound)}) :: {Guard(qexpr.Bound, qexpr.Difference, false)}({ExprToString(qexpr.Body)}))", + MachineAccessExpr max => MachineStateAdtSelectField(Deref(ExprToString(max.SubExpr)), max.Machine, + max.Entry), + SpecAccessExpr sax => $"{SpecPrefix}{sax.Spec.Name}_{sax.FieldName}", + EventAccessExpr eax => LabelAdtSelectPayloadField(ExprToString(eax.SubExpr), eax.PEvent, eax.Entry), + TestExpr { Kind: Machine m } texpr => MachineStateAdtIsM(Deref(ExprToString(texpr.Instance)), + m), // must deref because or else we don't have an ADT! + TestExpr { Kind: Event e } texpr => LabelAdtIsE(ExprToString(texpr.Instance), e), + TestExpr { Kind: State s } texpr => MachineStateAdtInS(Deref(ExprToString(texpr.Instance)), s.OwningMachine, + s), // must deref for ADT! + PureCallExpr pexpr => $"{pexpr.Pure.Name}({string.Join(", ", pexpr.Arguments.Select(ExprToString))})", + FlyingExpr fexpr => $"{InFlight(StateVar, ExprToString(fexpr.Instance))}", + SentExpr sexpr => $"{StateAdtSelectSent(StateVar)}[{ExprToString(sexpr.Instance)}]", + TargetsExpr texpr => + $"({LabelAdtSelectTarget(ExprToString(texpr.Instance))} == {ExprToString(texpr.Target)})", + _ => throw new NotSupportedException($"Not supported expr ({expr}) at {GetLocation(expr)}") + // _ => $"NotHandledExpr({expr})" + }; + + string BoundVars(List bound) + { + return $"{string.Join(", ", bound.Select(b => $"{LocalPrefix}{b.Name}: {TypeToString(b.Type)}"))}"; + } + + string Guard(List bound, bool difference, bool universal) + { + var impliesOrAnd = universal ? "==>" : "&&"; + + List bounds = []; + foreach (var b in bound) + { + switch (b.Type) + { + case PermissionType { Origin: Machine } pt: + bounds.Add(ExprToString(new TestExpr(b.SourceLocation, + new VariableAccessExpr(b.SourceLocation, b), pt.Origin))); + break; + case PermissionType { Origin: Interface } pt: + var name = pt.OriginalRepresentation; + + if (_globalScope.Lookup(name, out Machine m)) + { + bounds.Add(ExprToString(new TestExpr(b.SourceLocation, + new VariableAccessExpr(b.SourceLocation, b), m))); + } + + break; + case PermissionType { Origin: NamedEventSet } pt: + var e = ((NamedEventSet)pt.Origin).Events.First(); + bounds.Add(ExprToString(new TestExpr(b.SourceLocation, + new VariableAccessExpr(b.SourceLocation, b), e))); + if (difference) + { + bounds.Add($"{LocalPrefix}sent[{LocalPrefix}{b.Name}]"); + bounds.Add($"!{StateAdtSelectSent(StateVar)}[{LocalPrefix}{b.Name}]"); + } + + break; + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Event): + if (difference) + { + bounds.Add($"{LocalPrefix}sent[{LocalPrefix}{b.Name}]"); + bounds.Add($"!{StateAdtSelectSent(StateVar)}[{LocalPrefix}{b.Name}]"); + } + + break; + } + } + + if (bounds.Count != 0) + { + return "(" + string.Join(" && ", bounds) + $") {impliesOrAnd} "; + } + + return ""; + } + } + + private string NamedTupleExprHelper(NamedTupleExpr t) + { + var ty = (NamedTupleType)t.Type; + var names = ty.Fields.Select(f => f.Name); + var values = t.TupleFields.Select(ExprToString); + var args = string.Join(", ", names.Zip(values).Select(p => $"{p.First} := {p.Second}")); + return $"const_record({args})"; + } + + private static string BinOpToString(BinOpType op) + { + return op switch + { + BinOpType.Add => "+", + BinOpType.Sub => "-", + BinOpType.Mul => "*", + BinOpType.Div => "/", + BinOpType.Mod => "%", + BinOpType.Lt => "<", + BinOpType.Le => "<=", + BinOpType.Gt => ">", + BinOpType.Ge => ">=", + BinOpType.And => "&&", + BinOpType.Or => "||", + BinOpType.Eq => "==", + BinOpType.Neq => "!=", + BinOpType.Then => "==>", + BinOpType.Iff => "==", + _ => throw new NotImplementedException($"{op} is not implemented yet!") + }; + } + + private static string UnaryOpToString(UnaryOpType op) + { + return op switch + { + UnaryOpType.Negate => "-", + UnaryOpType.Not => "!", + _ => throw new NotImplementedException($"{op} is not implemented yet!") + }; + } + + private string TypeToString(PLanguageType t) + { + switch (t.Canonicalize()) + { + case NamedTupleType ntt: + var fields = string.Join(", ", + ntt.Fields.Select(nte => $"{nte.Name}: {TypeToString(nte.Type)}")); + return $"record {{{fields}}}"; + case PrimitiveType pt when pt.Equals(PrimitiveType.Bool): + return "boolean"; + case PrimitiveType pt when pt.Equals(PrimitiveType.Int): + return "integer"; + case PrimitiveType pt when pt.Equals(PrimitiveType.String): + return StringT; + case PrimitiveType pt when pt.Equals(PrimitiveType.Null): + return PNull; + case PrimitiveType pt when pt.Equals(PrimitiveType.Machine): + return MachineRefT; + case PrimitiveType pt when pt.Equals(PrimitiveType.Event): + return LabelAdt; + case TypeDefType tdt: + return $"{UserPrefix}{tdt.TypeDefDecl.Name}"; + case PermissionType { Origin: Machine } _: + return MachineRefT; + case PermissionType { Origin: Interface } _: + return MachineRefT; + case PermissionType { Origin: NamedEventSet } _: + return LabelAdt; + case EnumType et: + return $"{UserPrefix}{et.EnumDecl.Name}"; + case SetType st: + return $"[{TypeToString(st.ElementType)}]boolean"; + case MapType mt: + _optionsToDeclare.Add(mt.ValueType.Canonicalize()); + return $"[{TypeToString(mt.KeyType)}]{GetOptionName(mt.ValueType)}"; + } + + throw new NotSupportedException($"Not supported type expression {t} ({t.OriginalRepresentation})"); + } + + private string GetLocalName(Variable v) + { + return $"{LocalPrefix}{v.Name}"; + } + + + private string GetCheckerName(PLanguageType t) + { + var output = $"{CheckerPrefix}{TypeToString(t)}"; + return Regex.Replace(output, "[^a-zA-Z0-9_.]+", "", RegexOptions.Compiled); + } + + private string GetOptionName(PLanguageType t) + { + var output = $"{OptionPrefix}{TypeToString(t)}"; + return Regex.Replace(output, "[^a-zA-Z0-9_.]+", "", RegexOptions.Compiled); + } + + + private string GetChooseName(PLanguageType t) + { + var output = $"{ChoosePrefix}{TypeToString(t)}"; + return Regex.Replace(output, "[^a-zA-Z0-9_.]+", "", RegexOptions.Compiled); + } + + private string GetLocation(IPAST node) + { + return _ctx.LocationResolver.GetLocation(node.SourceLocation).ToString(); + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs b/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs index 7f20c153b0..8542172c60 100644 --- a/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs +++ b/Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs @@ -349,6 +349,8 @@ static private IPStmt ReplaceVars(IPStmt stmt, Dictionary var return new AnnounceStmt(announceStmt.SourceLocation, ReplaceVars(announceStmt.Event, varMap), ReplaceVars(announceStmt.Payload, varMap)); case AssertStmt assertStmt: return new AssertStmt(assertStmt.SourceLocation, ReplaceVars(assertStmt.Assertion, varMap), ReplaceVars(assertStmt.Message, varMap)); + case AssumeStmt assumeStmt: + return new AssumeStmt(assumeStmt.SourceLocation, ReplaceVars(assumeStmt.Assumption, varMap), ReplaceVars(assumeStmt.Message, varMap)); case AssignStmt assignStmt: return new AssignStmt(assignStmt.SourceLocation, ReplaceVars(assignStmt.Location, varMap), ReplaceVars(assignStmt.Value, varMap)); case CompoundStmt compoundStmt: diff --git a/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs b/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs index b8786954c7..3698c98f9b 100644 --- a/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs +++ b/Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs @@ -3,6 +3,7 @@ using Plang.Compiler.Backend.Java; using Plang.Compiler.Backend.Stately; using Plang.Compiler.Backend.Symbolic; +using Plang.Compiler.Backend.PVerifier; namespace Plang.Compiler.Backend { @@ -17,6 +18,7 @@ static TargetLanguage() RegisterCodeGenerator(CompilerOutput.Java, new JavaCompiler()); RegisterCodeGenerator(CompilerOutput.Symbolic, new SymbolicCodeGenerator()); RegisterCodeGenerator(CompilerOutput.Stately, new StatelyCodeGenerator()); + RegisterCodeGenerator(CompilerOutput.PVerifier, new PVerifierCodeGenerator()); } private static void RegisterCodeGenerator(CompilerOutput name, ICodeGenerator generator) diff --git a/Src/PCompiler/CompilerCore/Compiler.cs b/Src/PCompiler/CompilerCore/Compiler.cs index 99e94c02be..8205fbe72f 100644 --- a/Src/PCompiler/CompilerCore/Compiler.cs +++ b/Src/PCompiler/CompilerCore/Compiler.cs @@ -47,12 +47,23 @@ public int Compile(ICompilerConfiguration job) return Environment.ExitCode; } - // Convert functions to lowered SSA form with explicit cloning - foreach (var fun in scope.GetAllMethods()) + if (job.OutputLanguages.Contains(CompilerOutput.PVerifier)) { - IRTransformer.SimplifyMethod(fun); + // If using the PVerifier, don't output anything else + if (job.OutputLanguages.Count > 1) + { + throw new NotSupportedException("PVerifier backend must be used on its own!"); + } } - + else + { + // Convert functions to lowered SSA form with explicit cloning + foreach (var fun in scope.GetAllMethods()) + { + IRTransformer.SimplifyMethod(fun); + } + } + DirectoryInfo parentDirectory = job.OutputDirectory; foreach (var entry in job.OutputLanguages.Distinct()) { @@ -67,7 +78,10 @@ public int Compile(ICompilerConfiguration job) var compiledFiles = job.Backend.GenerateCode(job, scope); foreach (var file in compiledFiles) { - job.Output.WriteInfo($"Generated {file.FileName}."); + if (entry != CompilerOutput.PVerifier) + { + job.Output.WriteInfo($"Generated {file.FileName}."); + } job.Output.WriteFile(file); } @@ -107,6 +121,40 @@ private static PParser.ProgramContext Parse(ICompilerConfiguration job, FileInfo var fileStream = new AntlrInputStream(fileText); var lexer = new PLexer(fileStream); var tokens = new CommonTokenStream(lexer); + + if (!job.OutputLanguages.Contains(CompilerOutput.PVerifier)) + { + // disallow any pverifier tokens + tokens.Fill(); + foreach (var token in tokens.GetTokens()) + { + switch (token.Type) + { + case PParser.INVARIANT: + case PParser.AXIOM: + case PParser.IS: + case PParser.FLYING: + case PParser.TARGETS: + case PParser.SENT: + case PParser.PROOF: + case PParser.PROVE: + case PParser.USING: + case PParser.LEMMA: + case PParser.THEOREM: + case PParser.EXCEPT: + case PParser.REQUIRES: + case PParser.ENSURES: + case PParser.FORALL: + case PParser.EXISTS: + case PParser.INIT: + throw new NotSupportedException( + $"line {token.Line}:{token.Column} \"{token.Text}\" only supported by PVerifier backend."); + } + } + + tokens.Reset(); + } + var parser = new PParser(tokens); parser.RemoveErrorListeners(); @@ -156,6 +204,43 @@ public void SyntaxError(IRecognizer recognizer, IToken offendingSymbol, int line } } + public static Process NonBlockingRun(string activeDirectory, string exeName, params string[] argumentList) + { + var psi = new ProcessStartInfo(exeName) + { + CreateNoWindow = true, + UseShellExecute = false, + RedirectStandardError = true, + RedirectStandardInput = true, + RedirectStandardOutput = true, + WorkingDirectory = activeDirectory, + Arguments = string.Join(" ", argumentList) + }; + + var proc = new Process { StartInfo = psi }; + proc.Start(); + return proc; + } + + public static int WaitForResult(Process proc, out string stdout, out string stderr) + { + string mStderr = "", mStdout = ""; + proc.OutputDataReceived += (s, e) => { mStdout += $"{e.Data}\n"; }; + proc.ErrorDataReceived += (s, e) => + { + if (!string.IsNullOrWhiteSpace(e.Data)) + { + mStderr += $"{e.Data}\n"; + } + }; + proc.BeginErrorReadLine(); + proc.BeginOutputReadLine(); + proc.WaitForExit(); + stdout = mStdout; + stderr = mStderr; + return proc.ExitCode; + } + public static int RunWithOutput(string activeDirectory, out string stdout, out string stderr, string exeName, diff --git a/Src/PCompiler/CompilerCore/CompilerConfiguration.cs b/Src/PCompiler/CompilerCore/CompilerConfiguration.cs index 7c6c4db1aa..9eb06ef87d 100644 --- a/Src/PCompiler/CompilerCore/CompilerConfiguration.cs +++ b/Src/PCompiler/CompilerCore/CompilerConfiguration.cs @@ -24,6 +24,10 @@ public CompilerConfiguration() Backend = null; ProjectDependencies = new List(); Debug = false; + Timeout = 600; + HandlesAll = true; + CheckOnly = null; + Parallelism = Math.Max(Environment.ProcessorCount / 2, 1); } public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, IList outputLanguages, IList inputFiles, string projectName, DirectoryInfo projectRoot = null, IList projectDependencies = null, string pObservePackageName = null, bool debug = false) @@ -73,6 +77,10 @@ public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, IL public IList ProjectDependencies { get; set; } public bool Debug { get; set; } + public int Timeout { get; set; } + public bool HandlesAll { get; set; } + public string CheckOnly { get; set; } + public int Parallelism { get; set; } public void Copy(CompilerConfiguration parsedConfig) { diff --git a/Src/PCompiler/CompilerCore/CompilerCore.csproj b/Src/PCompiler/CompilerCore/CompilerCore.csproj index c3cf7ad18e..a226971419 100644 --- a/Src/PCompiler/CompilerCore/CompilerCore.csproj +++ b/Src/PCompiler/CompilerCore/CompilerCore.csproj @@ -9,6 +9,8 @@ + + diff --git a/Src/PCompiler/CompilerCore/CompilerOutput.cs b/Src/PCompiler/CompilerCore/CompilerOutput.cs index caada3e59b..225f8607cc 100644 --- a/Src/PCompiler/CompilerCore/CompilerOutput.cs +++ b/Src/PCompiler/CompilerCore/CompilerOutput.cs @@ -6,6 +6,7 @@ public enum CompilerOutput Symbolic, CSharp, Java, - Stately + Stately, + PVerifier, } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs index a9b99eee6e..0008b626ff 100644 --- a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs +++ b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs @@ -117,6 +117,17 @@ public Exception MissingNamedTupleEntry(PParser.IdenContext location, $"named tuple type {namedTuple.OriginalRepresentation} has no '{location.GetText()}' field"); } + public Exception MissingMachineField(PParser.IdenContext location, Machine machine) + { + return IssueError(location, + $"machine {machine.Name} has no '{location.GetText()}' field"); + } + public Exception MissingEventField(PParser.IdenContext location, Event pevent) + { + return IssueError(location, + $"machine {pevent.Name} payload has no '{location.GetText()}' field"); + } + public Exception OutOfBoundsTupleAccess(PParser.IntContext location, TupleType tuple) { return IssueError( diff --git a/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs b/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs index 1aa20f9dc8..584af4f849 100644 --- a/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs +++ b/Src/PCompiler/CompilerCore/ICompilerConfiguration.cs @@ -20,5 +20,9 @@ public interface ICompilerConfiguration ILocationResolver LocationResolver { get; } ITranslationErrorHandler Handler { get; } bool Debug { get; } + int Timeout { get; } + bool HandlesAll { get; } + string CheckOnly { get; } + int Parallelism { get; } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs index 5aea56f1d9..8d514b010e 100644 --- a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs +++ b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs @@ -37,6 +37,8 @@ Exception DuplicateStartState( Exception TypeMismatch(IPExpr expr, params TypeKind[] expected); Exception MissingNamedTupleEntry(PParser.IdenContext location, NamedTupleType namedTuple); + Exception MissingMachineField(PParser.IdenContext location, Machine machine); + Exception MissingEventField(PParser.IdenContext location, Event pevent); Exception OutOfBoundsTupleAccess(PParser.IntContext location, TupleType tuple); diff --git a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 b/Src/PCompiler/CompilerCore/Parser/PLexer.g4 index 8f7511ac8d..1474c310d6 100644 --- a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 +++ b/Src/PCompiler/CompilerCore/Parser/PLexer.g4 @@ -36,6 +36,7 @@ EXIT : 'exit' ; FOREACH : 'foreach'; FORMAT : 'format' ; FUN : 'fun' ; +PURE : 'pure' ; GOTO : 'goto' ; HALT : 'halt' ; HOT : 'hot' ; @@ -63,6 +64,25 @@ WHILE : 'while' ; WITH : 'with' ; CHOOSE : 'choose' ; +// PVerifier keywords +INVARIANT : 'invariant'; +AXIOM : 'axiom'; +IS : 'is'; +FLYING : 'inflight'; +TARGETS : 'targets'; +SENT : 'sent'; +PROOF : 'Proof'; +PROVE : 'prove'; +USING : 'using'; +LEMMA : 'Lemma'; +THEOREM : 'Theorem'; +EXCEPT : 'except'; +REQUIRES : 'requires'; +ENSURES : 'ensures'; +FORALL : 'forall' ; +EXISTS : 'exists' ; +INIT : 'init-condition'; + // module-system-specific keywords // module-test-implementation declarations @@ -109,6 +129,8 @@ NONDET : '$' ; LNOT : '!' ; LAND : '&&' ; LOR : '||' ; +LTHEN : '==>'; +LIFF : '<==>'; EQ : '==' ; NE : '!=' ; diff --git a/Src/PCompiler/CompilerCore/Parser/PParser.g4 b/Src/PCompiler/CompilerCore/Parser/PParser.g4 index dc00fca475..edc49f59a8 100644 --- a/Src/PCompiler/CompilerCore/Parser/PParser.g4 +++ b/Src/PCompiler/CompilerCore/Parser/PParser.g4 @@ -57,11 +57,24 @@ topDecl : typeDefDecl | implMachineDecl | specMachineDecl | funDecl + | pureDecl | namedModuleDecl | testDecl | implementationDecl + | invariantDecl + | invariantGroupDecl + | axiomDecl + | assumeOnStartDecl + | proofBlockDecl ; +invariantGroupDecl : LEMMA name=iden LBRACE invariantDecl* RBRACE + | THEOREM name=iden LBRACE invariantDecl* RBRACE + ; + +proofBlockDecl : PROOF LBRACE proofBody RBRACE ; +proofBody : proofItem* ; +proofItem : PROVE (targets+=expr (COMMA targets+=expr)* | goalsAll=MUL | goalsDefault=DEFAULT) (USING ((premises+=expr (COMMA premises+=expr)*) | premisesAll=MUL))? (EXCEPT excludes+=expr (COMMA excludes+=expr)*)? SEMI # ProveUsingCmd ; typeDefDecl : TYPE name=iden SEMI # ForeignTypeDef | TYPE name=iden ASSIGN type SEMI # PTypeDef @@ -105,7 +118,15 @@ varDecl : VAR idenList COLON type SEMI ; funDecl : FUN name=iden LPAREN funParamList? RPAREN (COLON type)? (CREATES interfaces+=iden)? SEMI # ForeignFunDecl | FUN name=iden LPAREN funParamList? RPAREN (COLON type)? functionBody # PFunDecl + | FUN name=iden LPAREN funParamList? RPAREN (RETURN LPAREN funParam RPAREN SEMI)? (REQUIRES requires+=expr SEMI)* (ENSURES ensures+=expr SEMI)* # ForeignFunDecl ; + +pureDecl : PURE name=iden LPAREN funParamList? RPAREN COLON type (ASSIGN body=expr)? SEMI ; + +invariantDecl: INVARIANT name=iden COLON body=expr SEMI ; +axiomDecl: AXIOM body=expr SEMI ; + +assumeOnStartDecl: INIT body=expr SEMI ; stateDecl : START? temperature=(HOT | COLD)? STATE name=iden LBRACE stateBodyItem* RBRACE ; @@ -133,6 +154,7 @@ stateName : state=iden ; functionBody : LBRACE varDecl* statement* RBRACE ; statement : LBRACE statement* RBRACE # CompoundStmt | ASSERT assertion=expr (COMMA message=expr)? SEMI # AssertStmt + | ASSUME assumption=expr (COMMA message=expr)? SEMI # AssumeStmt | PRINT message=expr SEMI # PrintStmt | RETURN expr? SEMI # ReturnStmt | BREAK SEMI # BreakStmt @@ -142,8 +164,9 @@ statement : LBRACE statement* RBRACE # CompoundStmt | lvalue INSERT LPAREN rvalue RPAREN SEMI # AddStmt | lvalue REMOVE expr SEMI # RemoveStmt | WHILE LPAREN expr RPAREN statement # WhileStmt - | FOREACH LPAREN item=iden IN collection=expr - RPAREN statement # ForeachStmt + | FOREACH LPAREN item=iden IN collection=expr RPAREN + (INVARIANT invariants+=expr SEMI)* + statement # ForeachStmt | IF LPAREN expr RPAREN thenBranch=statement (ELSE elseBranch=statement)? # IfStmt | NEW iden LPAREN rvalueList? RPAREN SEMI # CtorStmt @@ -173,6 +196,10 @@ expr : primitive # PrimitiveExpr | LPAREN expr RPAREN # ParenExpr | expr DOT field=iden # NamedTupleAccessExpr | expr DOT field=int # TupleAccessExpr + | instance=expr IS kind=iden # TestExpr + | instance=expr TARGETS target=expr # TargetsExpr + | FLYING instance=expr # FlyingExpr + | SENT instance=expr # SentExpr | seq=expr LBRACK index=expr RBRACK # SeqAccessExpr | fun=KEYS LPAREN expr RPAREN # KeywordExpr | fun=VALUES LPAREN expr RPAREN # KeywordExpr @@ -189,6 +216,12 @@ expr : primitive # PrimitiveExpr | lhs=expr op=(EQ | NE) rhs=expr # BinExpr | lhs=expr op=LAND rhs=expr # BinExpr | lhs=expr op=LOR rhs=expr # BinExpr + | lhs=expr op=LTHEN rhs=expr # BinExpr + | lhs=expr op=LIFF rhs=expr # BinExpr + | quant=(FORALL | EXISTS) + diff=NEW? + LPAREN bound=funParamList RPAREN + COLON COLON body=expr # QuantExpr | CHOOSE LPAREN expr? RPAREN # ChooseExpr | formatedString # StringExpr ; diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/AssumeOnStart.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/AssumeOnStart.cs new file mode 100644 index 0000000000..7d8cc0f53c --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/AssumeOnStart.cs @@ -0,0 +1,24 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Expressions; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class AssumeOnStart : IPDecl + { + public AssumeOnStart(string name, IPExpr body, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.AssumeOnStartDeclContext); + Body = body; + Name = name; + SourceLocation = sourceNode; + } + + public IPExpr Body { get; set; } + + public string Name { get; set; } + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Axiom.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Axiom.cs new file mode 100644 index 0000000000..a646cc76f3 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Axiom.cs @@ -0,0 +1,24 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Expressions; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class Axiom : IPDecl + { + public Axiom(string name, IPExpr body, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.AxiomDeclContext); + Name = name; + Body = body; + SourceLocation = sourceNode; + } + + public IPExpr Body { get; set; } + + public string Name { get; set; } + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs index 69ed97c4ad..519bdf4f2e 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs @@ -23,6 +23,8 @@ public class Function : IPDecl, IHasScope private readonly HashSet callees = new HashSet(); private readonly HashSet callers = new HashSet(); private readonly List localVariables = new List(); + private readonly List requireExprs = new List(); + private readonly List ensureExprs = new List(); private readonly List createsInterfaces = new List(); public Function(string name, ParserRuleContext sourceNode) @@ -57,6 +59,9 @@ public Function(ParserRuleContext sourceNode) : this("", sourceNode) public Function ParentFunction { get; set; } public FunctionSignature Signature { get; } = new FunctionSignature(); public IEnumerable LocalVariables => localVariables; + public Variable ReturnVariable { get; set; } + public IEnumerable Requires => requireExprs; + public IEnumerable Ensures => ensureExprs; public IEnumerable CreatesInterfaces => createsInterfaces; public FunctionRole Role { get; set; } @@ -70,7 +75,15 @@ public void AddLocalVariable(Variable local) { localVariables.Add(local); } - + public void AddRequire(IPExpr expr) + { + requireExprs.Add(expr); + } + public void AddEnsure(IPExpr expr) + { + ensureExprs.Add(expr); + } + public void RemoveLocalVariable(Variable local) { localVariables.Remove(local); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Invariant.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Invariant.cs new file mode 100644 index 0000000000..c70cc1a6bc --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Invariant.cs @@ -0,0 +1,34 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Expressions; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class Invariant : IPDecl + { + public Invariant(string name, IPExpr body, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.InvariantDeclContext); + IsDefault = false; + Name = name; + Body = body; + SourceLocation = sourceNode; + } + + public Invariant(ParserRuleContext sourceNode) + { + SourceLocation = sourceNode; + IsDefault = true; + Name = "defualt"; + } + + public IPExpr Body { get; set; } + + public string Name { get; set; } + + public bool IsDefault { get; } + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/InvariantGroup.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/InvariantGroup.cs new file mode 100644 index 0000000000..75689cbbe0 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/InvariantGroup.cs @@ -0,0 +1,17 @@ +using System.Collections.Generic; +using Antlr4.Runtime; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class InvariantGroup : IPDecl + { + public InvariantGroup(string name, ParserRuleContext sourceNode) + { + Name = name; + SourceLocation = sourceNode; + } + public List Invariants { get; set; } + public ParserRuleContext SourceLocation { get; } + public string Name { get; set; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs index 3b360419e8..f7dc50e146 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Generic; using System.Diagnostics; using System.Linq; @@ -83,5 +84,11 @@ public void AddFields(IEnumerable variables) { fields.AddRange(variables); } + + public bool LookupEntry(string name, out Variable entry) + { + var lookupTable = fields.ToDictionary(f => f.Name, f => f); + return lookupTable.TryGetValue(name, out entry); + } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/ProofCommand.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/ProofCommand.cs new file mode 100644 index 0000000000..91c9ef98fd --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/ProofCommand.cs @@ -0,0 +1,22 @@ +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class ProofCommand : IPDecl + { + public ProofCommand(string name, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.ProofItemContext); + SourceLocation = sourceNode; + Name = name; + } + + public List Goals { get; set; } + public List Premises { get; set; } + public List Excepts { get; set; } + public ParserRuleContext SourceLocation { get; } + public string Name { get; set; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Pure.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Pure.cs new file mode 100644 index 0000000000..acb93fdf78 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Pure.cs @@ -0,0 +1,27 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Statements; + +namespace Plang.Compiler.TypeChecker.AST.Declarations +{ + public class Pure : IPDecl, IHasScope + { + + public Pure(string name, ParserRuleContext sourceNode) + { + Debug.Assert(sourceNode is PParser.PureDeclContext); + Name = name; + SourceLocation = sourceNode; + } + + public FunctionSignature Signature { get; } = new FunctionSignature(); + + public string Name { get; set; } + public IPExpr Body { get; set; } + public ParserRuleContext SourceLocation { get; } + + public Scope Scope { get; set; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs index 30b3adc2b7..3172b00422 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BinOpType.cs @@ -16,7 +16,9 @@ public enum BinOpType Gt, Ge, And, - Or + Or, + Then, + Iff } public enum BinOpKind @@ -56,6 +58,8 @@ public static BinOpKind GetKind(this BinOpType op) // Boolean operators: case BinOpType.And: case BinOpType.Or: + case BinOpType.Then: + case BinOpType.Iff: return BinOpKind.Boolean; // This should be dead code. diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/EventAccessExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/EventAccessExpr.cs new file mode 100644 index 0000000000..7af5c1ced0 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/EventAccessExpr.cs @@ -0,0 +1,25 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class EventAccessExpr : IPExpr + { + public EventAccessExpr(ParserRuleContext sourceLocation, Event pevent, IPExpr subExpr, NamedTupleEntry entry) + { + SourceLocation = sourceLocation; + PEvent = pevent; + SubExpr = subExpr; + Entry = entry; + } + + public Event PEvent { get; } + public IPExpr SubExpr { get; } + public NamedTupleEntry Entry { get; } + public string FieldName => Entry.Name; + + public ParserRuleContext SourceLocation { get; } + public PLanguageType Type => Entry.Type; + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/FlyingExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/FlyingExpr.cs new file mode 100644 index 0000000000..2f24f3bb8e --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/FlyingExpr.cs @@ -0,0 +1,23 @@ +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class FlyingExpr : IPExpr + { + public FlyingExpr(ParserRuleContext sourceLocation, IPExpr instance) + { + SourceLocation = sourceLocation; + Instance = instance; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/InvariantRefExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/InvariantRefExpr.cs new file mode 100644 index 0000000000..5f3a4361ed --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/InvariantRefExpr.cs @@ -0,0 +1,35 @@ +using System.Collections.Generic; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class InvariantRefExpr : IPExpr + { + public InvariantRefExpr(Invariant inv, ParserRuleContext sourceLocation) + { + Invariant = inv; + SourceLocation = sourceLocation; + } + public Invariant Invariant { get; set; } + + public PLanguageType Type => PrimitiveType.Bool; + + public ParserRuleContext SourceLocation { get; set; } + } + + public class InvariantGroupRefExpr : IPExpr { + public InvariantGroupRefExpr(InvariantGroup invGroup, ParserRuleContext sourceLocation) + { + InvariantGroup = invGroup; + SourceLocation = sourceLocation; + } + public InvariantGroup InvariantGroup { get; set; } + public List Invariants => InvariantGroup.Invariants; + + public PLanguageType Type => PrimitiveType.Bool; + + public ParserRuleContext SourceLocation { get; set; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/MachineAccessExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/MachineAccessExpr.cs new file mode 100644 index 0000000000..e97d1c8d77 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/MachineAccessExpr.cs @@ -0,0 +1,25 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class MachineAccessExpr : IPExpr + { + public MachineAccessExpr(ParserRuleContext sourceLocation, Machine machine, IPExpr subExpr, Variable entry) + { + SourceLocation = sourceLocation; + Machine = machine; + SubExpr = subExpr; + Entry = entry; + } + + public Machine Machine { get; } + public IPExpr SubExpr { get; } + public Variable Entry { get; } + public string FieldName => Entry.Name; + + public ParserRuleContext SourceLocation { get; } + public PLanguageType Type => Entry.Type; + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/PureCallExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/PureCallExpr.cs new file mode 100644 index 0000000000..9470331dc8 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/PureCallExpr.cs @@ -0,0 +1,25 @@ +using System.Collections.Generic; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class PureCallExpr : IPExpr + { + public PureCallExpr(ParserRuleContext sourceLocation, Pure function, IReadOnlyList arguments) + { + SourceLocation = sourceLocation; + Pure = function; + Arguments = arguments; + Type = function.Signature.ReturnType; + } + + public Pure Pure { get; } + public IReadOnlyList Arguments { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantExpr.cs new file mode 100644 index 0000000000..160e0adcca --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantExpr.cs @@ -0,0 +1,30 @@ +using System.Collections.Generic; +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class QuantExpr : IPExpr + { + public QuantExpr(ParserRuleContext sourceLocation, QuantType operation, List bound, IPExpr body, bool difference) + { + SourceLocation = sourceLocation; + Quant = operation; + Bound = bound; + Body = body; + Difference = difference; + Type = PrimitiveType.Bool; + } + + public QuantType Quant { get; } + public List Bound { get; } + public IPExpr Body { get; } + public bool Difference { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantType.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantType.cs new file mode 100644 index 0000000000..3a00765fda --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/QuantType.cs @@ -0,0 +1,10 @@ +using System; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public enum QuantType + { + Forall, + Exists, + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SentExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SentExpr.cs new file mode 100644 index 0000000000..7b31d32d63 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SentExpr.cs @@ -0,0 +1,23 @@ +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class SentExpr : IPExpr + { + public SentExpr(ParserRuleContext sourceLocation, IPExpr instance) + { + SourceLocation = sourceLocation; + Instance = instance; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecAccessExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecAccessExpr.cs new file mode 100644 index 0000000000..845b416655 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecAccessExpr.cs @@ -0,0 +1,25 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class SpecAccessExpr : IPExpr + { + public SpecAccessExpr(ParserRuleContext sourceLocation, Machine machine, IPExpr subExpr, Variable entry) + { + SourceLocation = sourceLocation; + Spec = machine; + SubExpr = subExpr; + Entry = entry; + } + + public Machine Spec { get; } + public IPExpr SubExpr { get; } + public Variable Entry { get; } + public string FieldName => Entry.Name; + + public ParserRuleContext SourceLocation { get; } + public PLanguageType Type => Entry.Type; + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecRefExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecRefExpr.cs new file mode 100644 index 0000000000..e204d3ca50 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SpecRefExpr.cs @@ -0,0 +1,20 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class SpecRefExpr : IStaticTerm + { + public SpecRefExpr(ParserRuleContext sourceLocation, Machine value) + { + Value = value; + SourceLocation = sourceLocation; + } + + public Machine Value { get; } + + public PLanguageType Type { get; } = PrimitiveType.Machine; + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TargetsExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TargetsExpr.cs new file mode 100644 index 0000000000..36a9ffcfb5 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TargetsExpr.cs @@ -0,0 +1,25 @@ +using System.Diagnostics; +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class TargetsExpr : IPExpr + { + public TargetsExpr(ParserRuleContext sourceLocation, IPExpr instance, IPExpr target) + { + SourceLocation = sourceLocation; + Instance = instance; + Target = target; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + public IPExpr Target { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TestExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TestExpr.cs new file mode 100644 index 0000000000..63f08d7896 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TestExpr.cs @@ -0,0 +1,23 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class TestExpr : IPExpr + { + public TestExpr(ParserRuleContext sourceLocation, IPExpr instance, IPDecl kind) + { + SourceLocation = sourceLocation; + Instance = instance; + Kind = kind; + Type = PrimitiveType.Bool; + } + + public IPExpr Instance { get; } + public IPDecl Kind { get; } + + public ParserRuleContext SourceLocation { get; } + + public PLanguageType Type { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/AssumeStmt.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/AssumeStmt.cs new file mode 100644 index 0000000000..cd4b2dd947 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/AssumeStmt.cs @@ -0,0 +1,19 @@ +using Antlr4.Runtime; + +namespace Plang.Compiler.TypeChecker.AST.Statements +{ + public class AssumeStmt : IPStmt + { + public AssumeStmt(ParserRuleContext sourceLocation, IPExpr assumption, IPExpr message) + { + SourceLocation = sourceLocation; + Assumption = assumption; + Message = message; + } + + public IPExpr Assumption { get; } + public IPExpr Message { get; } + + public ParserRuleContext SourceLocation { get; } + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs index bcda223e7a..3d318d206a 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Statements/ForeachStmt.cs @@ -1,3 +1,4 @@ +using System.Collections.Generic; using Antlr4.Runtime; using Plang.Compiler.TypeChecker.AST.Declarations; @@ -5,17 +6,19 @@ namespace Plang.Compiler.TypeChecker.AST.Statements { public class ForeachStmt : IPStmt { - public ForeachStmt(ParserRuleContext sourceLocation, Variable item, IPExpr collection, IPStmt body) + public ForeachStmt(ParserRuleContext sourceLocation, Variable item, IPExpr collection, IPStmt body, List invariants) { SourceLocation = sourceLocation; Item = item; IterCollection = collection; Body = CompoundStmt.FromStatement(body); + Invariants = invariants; } public Variable Item { get; } public IPExpr IterCollection { get; } public CompoundStmt Body { get; } + public List Invariants { get; } public ParserRuleContext SourceLocation { get; } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs index d9679b59d9..f4ac74ca53 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs @@ -16,8 +16,8 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config, // Step 1: Build the global scope of declarations var globalScope = BuildGlobalScope(config, programUnits); - - // Step 2: Validate machine specifications + + // Step 2a: Validate machine specifications foreach (var machine in globalScope.Machines) { @@ -32,7 +32,7 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config, FunctionValidator.CheckAllPathsReturn(handler, machineFunction); } - // Step 2: Validate no static handlers + // Step 2b: Validate no static handlers foreach (var machine in globalScope.Machines) { MachineChecker.ValidateNoStaticHandlers(handler, machine); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs b/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs index ea09002934..75324dfbeb 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ControlFlowChecker.cs @@ -71,6 +71,7 @@ private void CheckStmt(IPStmt stmt) case AddStmt _: case AnnounceStmt _: case AssertStmt _: + case AssumeStmt _: case AssignStmt _: case CtorStmt _: case FunCallStmt _: diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs index 77782e7308..704f3b67fa 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs @@ -1,3 +1,5 @@ +using System; +using System.Linq; using Antlr4.Runtime.Misc; using Antlr4.Runtime.Tree; using Plang.Compiler.TypeChecker.AST; @@ -30,6 +32,60 @@ public static void PopulateStubs( visitor.Visit(context); } + public override object VisitInvariantDecl(PParser.InvariantDeclContext context) + { + var group = context.Parent as PParser.InvariantGroupDeclContext; + var name = group != null ? $"{group.name.GetText()}_PGROUP_{context.name.GetText()}": context.name.GetText(); + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return null; + } + + public override object VisitAxiomDecl(PParser.AxiomDeclContext context) + { + var name = $"axiom{CurrentScope.Axioms.Count()}"; + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return null; + } + + public override object VisitInvariantGroupDecl(PParser.InvariantGroupDeclContext context) + { + var name = context.name.GetText(); + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + context.invariantDecl().Select(Visit).ToList(); + return null; + } + + public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context) + { + var name = string.Join(", ", context._targets.Select(t => t.GetText())); + if (context._premises.Count > 0) + { + name += " using " + string.Join(", ", context._premises.Select(t => t.GetText())); + } + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return null; + } + + public override object VisitAssumeOnStartDecl(PParser.AssumeOnStartDeclContext context) + { + var name = $"init{CurrentScope.AssumeOnStarts.Count()}"; + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return null; + } + + public override object VisitPureDecl(PParser.PureDeclContext context) + { + var name = context.name.GetText(); + var decl = CurrentScope.Put(name, context); + nodesToDeclarations.Put(context, decl); + return VisitChildrenWithNewScope(decl, context); + } + #region Events public override object VisitEventDecl(PParser.EventDeclContext context) @@ -265,6 +321,10 @@ public override object VisitBinExpr(PParser.BinExprContext context) { return null; } + public override object VisitQuantExpr(PParser.QuantExprContext context) + { + return null; + } public override object VisitUnaryExpr(PParser.UnaryExprContext context) { @@ -380,6 +440,10 @@ public override object VisitAssertStmt(PParser.AssertStmtContext context) { return null; } + public override object VisitAssumeStmt(PParser.AssumeStmtContext context) + { + return null; + } public override object VisitReturnStmt(PParser.ReturnStmtContext context) { diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs index f29e8eb273..7842d719f1 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs @@ -2,9 +2,11 @@ using System.Collections.Generic; using System.Diagnostics; using System.Linq; +using Antlr4.Runtime; using Antlr4.Runtime.Tree; using Plang.Compiler.TypeChecker.AST; using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.AST.Expressions; using Plang.Compiler.TypeChecker.AST.States; using Plang.Compiler.TypeChecker.Types; using Plang.Compiler.Util; @@ -601,7 +603,193 @@ public override object VisitOnEventGotoState(PParser.OnEventGotoStateContext con } #endregion + + public override object VisitPureDecl(PParser.PureDeclContext context) + { + // PURE name=Iden body=Expr + var pure = (Pure) nodesToDeclarations.Get(context); + + // LPAREN funParamList? RPAREN + var paramList = context.funParamList() != null + ? (Variable[]) Visit(context.funParamList()) + : new Variable[0]; + pure.Signature.Parameters.AddRange(paramList); + + var temporaryFunction = new Function(pure.Name, context) + { + Scope = CurrentScope.MakeChildScope() + }; + + foreach (var p in paramList) + { + var param = temporaryFunction.Scope.Put(p.Name, p.SourceLocation, VariableRole.Param); + param.Type = p.Type; + nodesToDeclarations.Put(p.SourceLocation, param); + temporaryFunction.Signature.Parameters.Add(param); + } + + pure.Scope = temporaryFunction.Scope; + + // (COLON type)? + pure.Signature.ReturnType = ResolveType(context.type()); + + if (context.body is not null) + { + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + var body = exprVisitor.Visit(context.body); + + if (!pure.Signature.ReturnType.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, pure.Signature.ReturnType); + } + + pure.Body = body; + } + + return pure; + } + + public override object VisitInvariantDecl(PParser.InvariantDeclContext context) + { + // INVARIANT name=Iden body=Expr + var inv = (Invariant) nodesToDeclarations.Get(context); + + var temporaryFunction = new Function(inv.Name, context); + temporaryFunction.Scope = CurrentScope.MakeChildScope(); + + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + + var body = exprVisitor.Visit(context.body); + + if (!PrimitiveType.Bool.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool); + } + + inv.Body = body; + + return inv; + } + + public override object VisitAxiomDecl(PParser.AxiomDeclContext context) + { + // Axiom body=Expr + var inv = (Axiom) nodesToDeclarations.Get(context); + + var temporaryFunction = new Function(inv.Name, context); + temporaryFunction.Scope = CurrentScope.MakeChildScope(); + + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + + var body = exprVisitor.Visit(context.body); + + if (!PrimitiveType.Bool.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool); + } + + inv.Body = body; + + return inv; + } + + public override object VisitInvariantGroupDecl(PParser.InvariantGroupDeclContext context) + { + var invGroup = (InvariantGroup) nodesToDeclarations.Get(context); + invGroup.Invariants = context.invariantDecl().Select(Visit).Cast().ToList(); + return invGroup; + } + + private List ToInvariant(IPExpr e, ParserRuleContext context) + { + if (e is InvariantGroupRefExpr invGroupRef) return invGroupRef.Invariants; + if (e is InvariantRefExpr invRef) return [invRef.Invariant]; + if (!PrimitiveType.Bool.IsSameTypeAs(e.Type.Canonicalize())) + { + throw Handler.TypeMismatch(context, e.Type, PrimitiveType.Bool); + } + Invariant inv = new Invariant($"tmp_inv_{Guid.NewGuid()}", e, context); + return [inv]; + } + public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context) + { + var proofCmd = (ProofCommand) nodesToDeclarations.Get(context); + var temporaryFunction = new Function(proofCmd.Name, context); + temporaryFunction.Scope = CurrentScope.MakeChildScope(); + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + List premises = []; + List goals = []; + List excepts = context._excludes.Select(exprVisitor.Visit).ToList(); + if (context.premisesAll == null) + { + premises = context._premises.Select(exprVisitor.Visit).ToList(); + } + else + { + premises = CurrentScope.AllDecls.OfType().Select(x => (IPExpr) new InvariantRefExpr(x, context)).ToList(); + } + + if (context.goalsAll == null && context.goalsDefault == null) + { + goals = context._targets.Select(exprVisitor.Visit).ToList(); + } + else if (context.goalsDefault != null) + { + goals = [new InvariantRefExpr(new Invariant(context), context)]; + } + else + { + goals = CurrentScope.AllDecls.OfType().Select(x => (IPExpr) new InvariantRefExpr(x, context)).ToList(); + } + + if (premises.Count == context._premises.Count) + { + proofCmd.Premises = premises.Zip(context._premises, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList(); + } + else + { + proofCmd.Premises = premises.SelectMany(x => ToInvariant(x, context)).ToList(); + } + + if (goals.Count == context._targets.Count) + { + proofCmd.Goals = goals.Zip(context._targets, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList(); + } + else + { + proofCmd.Goals = goals.SelectMany(x => ToInvariant(x, context)).ToList(); + } + + proofCmd.Excepts = excepts.Zip(context._excludes, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList(); + // exclude things appear in `goals` from `premises` + proofCmd.Premises = proofCmd.Premises.Except(proofCmd.Goals).Except(proofCmd.Excepts).ToList(); + proofCmd.Goals = proofCmd.Goals.Except(proofCmd.Excepts).ToList(); + return proofCmd; + } + + public override object VisitAssumeOnStartDecl(PParser.AssumeOnStartDeclContext context) + { + // assume on start: body=Expr + var assume = (AssumeOnStart) nodesToDeclarations.Get(context); + + var temporaryFunction = new Function(assume.Name, context); + temporaryFunction.Scope = CurrentScope.MakeChildScope(); + + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + + var body = exprVisitor.Visit(context.body); + + if (!PrimitiveType.Bool.IsSameTypeAs(body.Type)) + { + throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool); + } + + assume.Body = body; + + return assume; + } + #region Functions public override object VisitPFunDecl(PParser.PFunDeclContext context) @@ -649,6 +837,40 @@ public override object VisitForeignFunDecl(PParser.ForeignFunDeclContext context else throw Handler.MissingDeclaration(createdInterface, "interface", createdInterface.GetText()); } + + + var temporaryFunction = new Function(fun.Name, context); + temporaryFunction.Scope = fun.Scope.MakeChildScope(); + + // (RETURN LPAREN funParam RPAREN SEMI)? + if (context.funParam() != null) + { + Variable p = (Variable)Visit(context.funParam()); + // Add the return variable to the scope so that contracts can refer to it + var ret = temporaryFunction.Scope.Put(p.Name, p.SourceLocation, VariableRole.Param); + ret.Type = p.Type; + nodesToDeclarations.Put(p.SourceLocation, ret); + temporaryFunction.Signature.Parameters.Add(ret); + + fun.ReturnVariable = ret; + // update the return type to match + fun.Signature.ReturnType = fun.ReturnVariable.Type; + } + + var exprVisitor = new ExprVisitor(temporaryFunction, Handler); + + // (REQUIRES requires+=expr SEMI)* + foreach (var req in context._requires) + { + fun.AddRequire(exprVisitor.Visit(req)); + } + + // (ENSURES ensures+=expr SEMI)* + foreach (var ensure in context._ensures) + { + fun.AddEnsure(exprVisitor.Visit(ensure)); + } + return fun; } diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs index ff6d1e2d0d..2525a1e272 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs @@ -6,6 +6,7 @@ using Plang.Compiler.TypeChecker.AST; using Plang.Compiler.TypeChecker.AST.Declarations; using Plang.Compiler.TypeChecker.AST.Expressions; +using Plang.Compiler.TypeChecker.AST.States; using Plang.Compiler.TypeChecker.Types; namespace Plang.Compiler.TypeChecker @@ -14,7 +15,7 @@ public class ExprVisitor : PParserBaseVisitor { private readonly ITranslationErrorHandler handler; private readonly Function method; - private readonly Scope table; + private Scope table; public ExprVisitor(Function method, ITranslationErrorHandler handler) { @@ -45,18 +46,82 @@ public override IPExpr VisitParenExpr(PParser.ParenExprContext context) public override IPExpr VisitNamedTupleAccessExpr(PParser.NamedTupleAccessExprContext context) { - var subExpr = Visit(context.expr()); - if (!(subExpr.Type.Canonicalize() is NamedTupleType tuple)) - { - throw handler.TypeMismatch(subExpr, TypeKind.NamedTuple); - } + IPExpr subExpr = Visit(context.expr()); var fieldName = context.field.GetText(); - if (!tuple.LookupEntry(fieldName, out var entry)) + + switch (subExpr.Type.Canonicalize()) { - throw handler.MissingNamedTupleEntry(context.field, tuple); - } + case NamedTupleType tuple: + if (!tuple.LookupEntry(fieldName, out var entry)) + { + throw handler.MissingNamedTupleEntry(context.field, tuple); + } + + return new NamedTupleAccessExpr(context, subExpr, entry); + + case PermissionType {Origin: Machine} permission: + var machine = (Machine) permission.Origin; + + if (!machine.LookupEntry(fieldName, out var field)) + { + throw handler.MissingMachineField(context.field, machine); + } + return new MachineAccessExpr(context, machine, subExpr, field); + + case PermissionType {Origin: Interface} permission: + var pname = permission.Origin.Name; + + if (!table.Lookup(pname, out Machine m)) + { + throw handler.TypeMismatch(subExpr, [TypeKind.NamedTuple, TypeKind.Base]); + } + + if (!m.LookupEntry(fieldName, out var mfield)) + { + throw handler.MissingMachineField(context.field, m); + } + return new MachineAccessExpr(context, m, subExpr, mfield); + + case PermissionType {Origin: NamedEventSet} permission: - return new NamedTupleAccessExpr(context, subExpr, entry); + var pevents = ((NamedEventSet)permission.Origin).Events.ToList(); + + foreach (var pevent in pevents) + { + switch (pevent.PayloadType.Canonicalize()) + { + case NamedTupleType namedTupleType: + if (namedTupleType.LookupEntry(fieldName, out var pentry)) + { + return new EventAccessExpr(context, pevent, subExpr, pentry); + } + break; + } + } + + throw handler.MissingEventField(context.field, pevents.First()); + + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Machine): + Machine spec; + + switch (subExpr) + { + case SpecRefExpr specRefExpr: + spec = specRefExpr.Value; + break; + default: + throw handler.TypeMismatch(subExpr, [TypeKind.NamedTuple, TypeKind.Base]); + } + + if (!spec.LookupEntry(fieldName, out var sfield)) + { + throw handler.MissingMachineField(context.field, spec); + } + return new SpecAccessExpr(context, spec, subExpr, sfield); + + default: + throw handler.TypeMismatch(subExpr, [TypeKind.NamedTuple, TypeKind.Base]); + } } public override IPExpr VisitTupleAccessExpr(PParser.TupleAccessExprContext context) @@ -180,33 +245,68 @@ public override IPExpr VisitCtorExpr(PParser.CtorExprContext context) public override IPExpr VisitFunCallExpr(PParser.FunCallExprContext context) { var funName = context.fun.GetText(); - if (!table.Lookup(funName, out Function function)) + if (table.Lookup(funName, out Function function)) { - throw handler.MissingDeclaration(context.fun, "function", funName); - } + // Check the arguments + var arguments = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), this).ToArray(); + ISet linearVariables = new System.Collections.Generic.HashSet(); - // Check the arguments - var arguments = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), this).ToArray(); - ISet linearVariables = new HashSet(); + if (function.Signature.Parameters.Count != arguments.Length) + { + throw handler.IncorrectArgumentCount(context, arguments.Length, function.Signature.Parameters.Count); + } - if (function.Signature.Parameters.Count != arguments.Length) - { - throw handler.IncorrectArgumentCount(context, arguments.Length, function.Signature.Parameters.Count); - } + for (var i = 0; i < arguments.Length; i++) + { + var argument = arguments[i]; + var paramType = function.Signature.Parameters[i].Type; + if (!paramType.IsAssignableFrom(argument.Type)) + { + throw handler.TypeMismatch(context.rvalueList().rvalue(i), argument.Type, paramType); + } + + } - for (var i = 0; i < arguments.Length; i++) + method.AddCallee(function); + return new FunCallExpr(context, function, arguments); + } + if (table.Lookup(funName, out Pure pure)) { - var argument = arguments[i]; - var paramType = function.Signature.Parameters[i].Type; - if (!paramType.IsAssignableFrom(argument.Type)) + // Check the arguments + var arguments = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), this).ToArray(); + ISet linearVariables = new System.Collections.Generic.HashSet(); + + if (pure.Signature.Parameters.Count != arguments.Length) { - throw handler.TypeMismatch(context.rvalueList().rvalue(i), argument.Type, paramType); + throw handler.IncorrectArgumentCount(context, arguments.Length, pure.Signature.Parameters.Count); } + for (var i = 0; i < arguments.Length; i++) + { + var argument = arguments[i]; + var paramType = pure.Signature.Parameters[i].Type; + if (!paramType.IsAssignableFrom(argument.Type)) + { + switch (paramType) + { + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Event): + switch (argument.Type) + { + case PermissionType {Origin: NamedEventSet} per when ((NamedEventSet)(per.Origin)).Events.Count() == 1: + continue; + } + break; + } + throw handler.TypeMismatch(context.rvalueList().rvalue(i), argument.Type, paramType); + } + + } + + return new PureCallExpr(context, pure, arguments); } + + throw handler.MissingDeclaration(context.fun, "function", funName); - method.AddCallee(function); - return new FunCallExpr(context, function, arguments); } public override IPExpr VisitUnaryExpr(PParser.UnaryExprContext context) @@ -240,6 +340,100 @@ public override IPExpr VisitUnaryExpr(PParser.UnaryExprContext context) } } + public override IPExpr VisitQuantExpr(PParser.QuantExprContext context) + { + var oldTable = table; + table = table.MakeChildScope(); + + bool diff = context.diff != null; + + var bound = context.bound.funParam().Select(p => + { + var symbolName = p.name.GetText(); + var param = table.Put(symbolName, p, VariableRole.Param); + param.Type = TypeResolver.ResolveType(p.type(), table, handler); + return param; + }).Cast().ToArray(); + + if (diff && bound.ToList().Count != 1) + { + // we have the "new" annotation so the bound must be a single thing and it must be an event + throw handler.InternalError(context, new ArgumentException($"Difference quantifiers must have exactly one bound variable", nameof(context))); + } + + if (diff) + { + switch (bound[0].Type.Canonicalize()) + { + case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Event): + break; + case PermissionType {Origin: NamedEventSet} _: + break; + default: + throw handler.TypeMismatch(context.bound, bound[0].Type, PrimitiveType.Event); + } + } + + var body = Visit(context.body); + + table = oldTable; + + if (context.quant.Text == "forall") + { + return new QuantExpr(context, QuantType.Forall, bound.ToList(), body, diff); + } + + return new QuantExpr(context, QuantType.Exists, bound.ToList(), body, diff); + } + + public override IPExpr VisitTestExpr(PParser.TestExprContext context) + { + var instance = Visit(context.instance); + string name = context.kind.GetText(); + + if (table.Lookup(name, out Machine m)) + { + return new TestExpr(context, instance, m); + } + + if (table.Lookup(name, out Event e)) + { + return new TestExpr(context, instance, e); + } + + if (table.Lookup(name, out State s)) + { + return new TestExpr(context, instance, s); + } + + throw handler.MissingDeclaration(context, "machine, event, or state", name); + } + + public override IPExpr VisitTargetsExpr(PParser.TargetsExprContext context) + { + var instance = Visit(context.instance); + var target = Visit(context.target); + + // TODO: type check to make sure instance is an event and machine is a machine + return new TargetsExpr(context, instance, target); + } + + public override IPExpr VisitFlyingExpr(PParser.FlyingExprContext context) + { + var instance = Visit(context.instance); + + // TODO: type check to make sure instance is an event + return new FlyingExpr(context, instance); + } + + public override IPExpr VisitSentExpr(PParser.SentExprContext context) + { + var instance = Visit(context.instance); + + // TODO: type check to make sure instance is an event + return new SentExpr(context, instance); + } + public override IPExpr VisitBinExpr(PParser.BinExprContext context) { var lhs = Visit(context.lhs); @@ -262,7 +456,9 @@ public override IPExpr VisitBinExpr(PParser.BinExprContext context) var logicCtors = new Dictionary> { {"&&", (elhs, erhs) => new BinOpExpr(context, BinOpType.And, elhs, erhs)}, - {"||", (elhs, erhs) => new BinOpExpr(context, BinOpType.Or, elhs, erhs)} + {"||", (elhs, erhs) => new BinOpExpr(context, BinOpType.Or, elhs, erhs)}, + {"==>", (elhs, erhs) => new BinOpExpr(context, BinOpType.Then, elhs, erhs)}, + {"<==>", (elhs, erhs) => new BinOpExpr(context, BinOpType.Iff, elhs, erhs)} }; var compCtors = new Dictionary> @@ -349,7 +545,9 @@ public override IPExpr VisitBinExpr(PParser.BinExprContext context) return compCtors[op](lhs, rhs); case "&&": - case "||": + case "||": + case "==>": + case "<==>": if (!PrimitiveType.Bool.IsAssignableFrom(lhs.Type)) { throw handler.TypeMismatch(context.lhs, lhs.Type, PrimitiveType.Bool); @@ -517,7 +715,22 @@ public override IPExpr VisitPrimitive(PParser.PrimitiveContext context) return new EventRefExpr(context, evt); } - throw handler.MissingDeclaration(context.iden(), "variable, enum element, or event", symbolName); + if (table.Lookup(symbolName, out Machine mac) && mac.IsSpec) + { + return new SpecRefExpr(context, mac); + } + + if (table.Lookup(symbolName, out Invariant inv)) + { + return new InvariantRefExpr(inv, context); + } + + if (table.Lookup(symbolName, out InvariantGroup invGroup)) + { + return new InvariantGroupRefExpr(invGroup, context); + } + + throw handler.MissingDeclaration(context.iden(), "variable, enum element, spec machine, or event", symbolName); } if (context.floatLiteral() != null) @@ -598,7 +811,7 @@ public override IPExpr VisitNamedTupleBody(PParser.NamedTupleBodyContext context var fields = context._values.Select(Visit).ToArray(); var entries = new NamedTupleEntry[fields.Length]; - var names = new HashSet(); + var names = new System.Collections.Generic.HashSet(); for (var i = 0; i < fields.Length; i++) { var entryName = context._names[i].GetText(); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs b/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs index 16b1204a1a..5a765e030e 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/FunctionValidator.cs @@ -40,6 +40,10 @@ public static bool SurelyReturns(IPStmt stmt) when (assertStmt.Assertion as BoolLiteralExpr)?.Value == false: return true; + case AssumeStmt assumeStmt + when (assumeStmt.Assumption as BoolLiteralExpr)?.Value == false: + return true; + case GotoStmt _: return true; diff --git a/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs b/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs index 4327ed099c..974e492417 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs @@ -53,6 +53,10 @@ private static IEnumerable InferCreates(IPAST tree, ITranslationError case AssertStmt assertStmt: return InferCreatesForExpr(assertStmt.Assertion, handler) .Union(InferCreatesForExpr(assertStmt.Message, handler)); + + case AssumeStmt assumeStmt: + return InferCreatesForExpr(assumeStmt.Assumption, handler) + .Union(InferCreatesForExpr(assumeStmt.Message, handler)); case AssignStmt assignStmt: return InferCreatesForExpr(assignStmt.Location, handler) diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs b/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs index 7ee7cdcdf3..ea85b509e8 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs @@ -130,7 +130,7 @@ private void CheckWellFormedness(AssertModuleExpr assertExpr) currentModule.InterfaceDef.Add(ipItem.Key, ipItem.Value); } } - + internal void CheckRefinementTest(RefinementTest test) { //check that the test module is closed with respect to creates diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs b/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs index da78441999..54f013d5bd 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs @@ -22,6 +22,12 @@ public class Scope private readonly IDictionary events = new Dictionary(); private readonly IDictionary eventSets = new Dictionary(); private readonly IDictionary functions = new Dictionary(); + private readonly IDictionary pures = new Dictionary(); + private readonly IDictionary invariants = new Dictionary(); + private readonly IDictionary axioms = new Dictionary(); + private readonly List<(string, ProofCommand)> proofCommands = new List<(string, ProofCommand)>(); + private readonly IDictionary invariantGroups = new Dictionary(); + private readonly IDictionary assumeOnStarts = new Dictionary(); private readonly ICompilerConfiguration config; private readonly IDictionary implementations = new Dictionary(); private readonly IDictionary interfaces = new Dictionary(); @@ -56,6 +62,10 @@ private Scope(ICompilerConfiguration config, Scope parent = null) .Concat(Events) .Concat(EventSets) .Concat(Functions) + .Concat(Invariants) + .Concat(Axioms) + .Concat(AssumeOnStarts) + .Concat(Pures) .Concat(Interfaces) .Concat(Machines) .Concat(States) @@ -71,6 +81,10 @@ private Scope(ICompilerConfiguration config, Scope parent = null) public IEnumerable Events => events.Values; public IEnumerable EventSets => eventSets.Values; public IEnumerable Functions => functions.Values; + public IEnumerable Invariants => invariants.Values; + public IEnumerable Axioms => axioms.Values; + public IEnumerable AssumeOnStarts => assumeOnStarts.Values; + public IEnumerable Pures => pures.Values; public IEnumerable Interfaces => interfaces.Values; public IEnumerable Machines => machines.Values; public IEnumerable States => states.Values; @@ -81,6 +95,8 @@ private Scope(ICompilerConfiguration config, Scope parent = null) public IEnumerable RefinementTests => refinementTests.Values; public IEnumerable Implementations => implementations.Values; public IEnumerable NamedModules => namedModules.Values; + public IEnumerable ProofCommands => proofCommands.Select(p => p.Item2); + public IEnumerable InvariantGroups => invariantGroups.Values; public static Scope CreateGlobalScope(ICompilerConfiguration config) { @@ -160,6 +176,37 @@ public bool Get(string name, out Function tree) { return functions.TryGetValue(name, out tree); } + + public bool Get(string name, out Invariant tree) + { + return invariants.TryGetValue(name, out tree); + } + + public bool Get(string name, out InvariantGroup tree) + { + return invariantGroups.TryGetValue(name, out tree); + } + + public bool Get(string name, out Axiom tree) + { + return axioms.TryGetValue(name, out tree); + } + + public bool Get(string name, out ProofCommand tree) + { + tree = proofCommands.Find(x => x.Item1 == name).Item2; + return tree != null; + } + + public bool Get(string name, out AssumeOnStart tree) + { + return assumeOnStarts.TryGetValue(name, out tree); + } + + public bool Get(string name, out Pure tree) + { + return pures.TryGetValue(name, out tree); + } public bool Get(string name, out Interface tree) { @@ -294,7 +341,92 @@ public bool Lookup(string name, out Function tree) tree = null; return false; } + + public bool Lookup(string name, out Invariant tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + + current = current.Parent; + } + + tree = null; + return false; + } + + public bool Lookup(string name, out InvariantGroup tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + + current = current.Parent; + } + + tree = null; + return false; + } + + public bool Lookup(string name, out Axiom tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + + current = current.Parent; + } + + tree = null; + return false; + } + + public bool Lookup(string name, out ProofCommand tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + + current = current.Parent; + } + + tree = null; + return false; + } + + public bool Lookup(string name, out Pure tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + return true; + } + current = current.Parent; + } + + tree = null; + return false; + } + public bool Lookup(string name, out Interface tree) { var current = this; @@ -339,6 +471,16 @@ public bool Lookup(string name, out State tree) return true; } + // look inside machines to find the state. + // TODO: bug if multiple machines have the same state name + foreach (var m in current.Machines) + { + if (m.Scope.Get(name, out tree)) + { + return true; + } + } + current = current.Parent; } @@ -548,6 +690,54 @@ public Function Put(string name, PParser.FunDeclContext tree) return function; } + + public Pure Put(string name, PParser.PureDeclContext tree) + { + var pure = new Pure(name, tree); + CheckConflicts(pure, Namespace(pures)); + pures.Add(name, pure); + return pure; + } + + public Invariant Put(string name, PParser.InvariantDeclContext tree) + { + var invariant = new Invariant(name, null, tree); // need to add expr later + CheckConflicts(invariant, Namespace(invariants)); + invariants.Add(name, invariant); + return invariant; + } + + public InvariantGroup Put(string name, PParser.InvariantGroupDeclContext tree) + { + var group = new InvariantGroup(name, tree); + CheckConflicts(group, Namespace(invariantGroups)); + invariantGroups.Add(name, group); + return group; + } + + public Axiom Put(string name, PParser.AxiomDeclContext tree) + { + var axiom = new Axiom(name, null, tree); // need to add expr later + CheckConflicts(axiom, Namespace(axioms)); + axioms.Add(name, axiom); + return axiom; + } + + public ProofCommand Put(string name, PParser.ProofItemContext tree) + { + var proofCommand = new ProofCommand(name, tree); + proofCommands.Add((name, proofCommand)); + return proofCommand; + } + + public AssumeOnStart Put(string name, PParser.AssumeOnStartDeclContext tree) + { + var assumeOnStart = new AssumeOnStart(name, null, tree); // need to add expr later + CheckConflicts(assumeOnStart, Namespace(assumeOnStarts)); + assumeOnStarts.Add(name, assumeOnStart); + return assumeOnStart; + } + public EnumElem Put(string name, PParser.EnumElemContext tree) { var enumElem = new EnumElem(name, tree); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs index 16604ee817..caa917184f 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs @@ -63,6 +63,30 @@ public override IPStmt VisitAssertStmt(PParser.AssertStmtContext context) return new AssertStmt(context, assertion, assertMessage); } + + + public override IPStmt VisitAssumeStmt(PParser.AssumeStmtContext context) + { + var assumption = exprVisitor.Visit(context.assumption); + if (!PrimitiveType.Bool.IsSameTypeAs(assumption.Type)) + { + throw handler.TypeMismatch(context.assumption, assumption.Type, PrimitiveType.Bool); + } + IPExpr assertMessage = new StringExpr(context, @$"{config.LocationResolver.GetLocation(context).ToString().Replace(@"\", @"\\")}",new List()); + if (context.message != null) + { + var message = exprVisitor.Visit(context.message); + if (!message.Type.IsSameTypeAs(PrimitiveType.String)) + { + throw handler.TypeMismatch(context.message, message.Type, PrimitiveType.String); + } + + assertMessage = new StringExpr(message.SourceLocation, "{0} {1}",new List() {assertMessage, + message}); + } + + return new AssumeStmt(context, assumption, assertMessage); + } public override IPStmt VisitPrintStmt(PParser.PrintStmtContext context) { @@ -258,9 +282,12 @@ public override IPStmt VisitForeachStmt(PParser.ForeachStmtContext context) throw handler.TypeMismatch(context.item, itemType, expectedItemType); var body = Visit(context.statement()); - return new ForeachStmt(context, var, collection, body); - } + var invs = context._invariants.Select(exprVisitor.Visit).ToList(); + + return new ForeachStmt(context, var, collection, body, invs); + } + public override IPStmt VisitIfStmt(PParser.IfStmtContext context) { var condition = exprVisitor.Visit(context.expr()); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs b/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs index 39b22c3681..a5d06d2d6b 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/TypeResolver.cs @@ -93,6 +93,13 @@ public override PLanguageType VisitNamedType(PParser.NamedTypeContext context) { return new PermissionType(machine); } + + if (scope.Lookup(typeName, out Event pevent)) + { + var eset = new NamedEventSet(pevent.Name, pevent.SourceLocation); + eset.AddEvent(pevent); + return new PermissionType(eset); + } throw handler.MissingDeclaration(context.name, "enum, typedef, event set, machine, or interface", typeName); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs b/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs index 6c96452550..db475dddd3 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Types/PermissionType.cs @@ -8,28 +8,28 @@ namespace Plang.Compiler.TypeChecker.Types { public class PermissionType : PLanguageType { - private readonly IPDecl origin; - public PermissionType(Machine machine) : base(TypeKind.Base) { - origin = machine; + Origin = machine; AllowedPermissions = new Lazy>(() => machine.Receives.Events.ToList()); } public PermissionType(Interface pInterface) : base(TypeKind.Base) { - origin = pInterface; + Origin = pInterface; AllowedPermissions = new Lazy>(() => pInterface.ReceivableEvents.Events.ToList()); } public PermissionType(NamedEventSet eventSet) : base(TypeKind.Base) { - origin = eventSet; + Origin = eventSet; AllowedPermissions = new Lazy>(() => eventSet.Events.ToList()); } + + public IPDecl Origin { get; } - public override string OriginalRepresentation => origin.Name; - public override string CanonicalRepresentation => origin.Name; + public override string OriginalRepresentation => Origin.Name; + public override string CanonicalRepresentation => Origin.Name; public override Lazy> AllowedPermissions { get; } diff --git a/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs index a6a3b88ed2..00a4e4ca0a 100644 --- a/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs +++ b/Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs @@ -45,6 +45,12 @@ internal PCompilerOptions() Parser.AddArgument("pobserve-package", "po", "PObserve package name").IsHidden = true; Parser.AddArgument("debug", "d", "Enable debug logs", typeof(bool)).IsHidden = true; + + Parser.AddArgument("timeout", "t", "Set SMT solver timeout in seconds", typeof(int)).IsHidden = true; + + Parser.AddArgument("no-event-handler-checks", "nch", "Do not check that all events are handled", typeof(bool)).IsHidden = true; + Parser.AddArgument("check-only", "co", "Check only the specified machine", typeof(string)).IsHidden = true; + Parser.AddArgument("jobs", "j", "Number of parallel processes to use", typeof(int)).IsHidden = true; } /// @@ -161,6 +167,18 @@ private static void UpdateConfigurationWithParsedArgument(CompilerConfiguration case "debug": compilerConfiguration.Debug = true; break; + case "timeout": + compilerConfiguration.Timeout = (int)option.Value; + break; + case "no-event-handler-checks": + compilerConfiguration.HandlesAll = false; + break; + case "check-only": + compilerConfiguration.CheckOnly = (string)option.Value; + break; + case "jobs": + compilerConfiguration.Parallelism = (int)option.Value; + break; case "mode": compilerConfiguration.OutputLanguages = new List(); switch (((string)option.Value).ToLowerInvariant()) diff --git a/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs b/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs index ceb53c7016..1c9b2742ae 100644 --- a/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs +++ b/Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs @@ -242,9 +242,12 @@ private IList GetTargetLanguages(FileInfo fullPathName) case "stately": outputLanguages.Add(CompilerOutput.Stately); break; + case "pverifier": + outputLanguages.Add(CompilerOutput.PVerifier); + break; default: throw new CommandlineParsingError( - $"Expected CSharp, Java, Stately, or Symbolic as target, received {projectXml.Element("Target")?.Value}"); + $"Expected CSharp, Java, Stately, PVerifier, or Symbolic as target, received {projectXml.Element("Target")?.Value}"); } } } diff --git a/Tutorial/Advanced/1_ChainReplicationVerification/.gitignore b/Tutorial/Advanced/1_ChainReplicationVerification/.gitignore new file mode 100644 index 0000000000..161a65f6d8 --- /dev/null +++ b/Tutorial/Advanced/1_ChainReplicationVerification/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tutorial/Advanced/1_ChainReplicationVerification/ChainReplicationVerification.pproj b/Tutorial/Advanced/1_ChainReplicationVerification/ChainReplicationVerification.pproj new file mode 100644 index 0000000000..10a22b1b80 --- /dev/null +++ b/Tutorial/Advanced/1_ChainReplicationVerification/ChainReplicationVerification.pproj @@ -0,0 +1,8 @@ + +ChainReplicationVerification + + ./PSrc/ + +./PGenerated/ +PVerifier + diff --git a/Tutorial/Advanced/1_ChainReplicationVerification/PSrc/System.p b/Tutorial/Advanced/1_ChainReplicationVerification/PSrc/System.p new file mode 100644 index 0000000000..a6e36f1cf2 --- /dev/null +++ b/Tutorial/Advanced/1_ChainReplicationVerification/PSrc/System.p @@ -0,0 +1,128 @@ +type tWriteRequest = (source: machine, k: int, v: int); +type tReadRequest = (source: machine, k: int); +type tReadResponse = (source: machine, k: int, v: int, status: bool); + +event eWriteRequest : tWriteRequest; +event eWriteResponse : tWriteRequest; + +event ePropagateWrite: tWriteRequest; + +event eReadRequest : tReadRequest; +event eReadResponse : tReadResponse; + +machine Head { + var kv: map[int, int]; + + start state Receiving { + on eWriteRequest do (req: tWriteRequest) { + kv[req.k] = req.v; + send next_(this), ePropagateWrite, (source = req.source, k = req.k, v = req.v); + } + } +} + +machine Body { + var kv: map[int, int]; + + start state Forwarding { + on ePropagateWrite do (req: tWriteRequest) { + kv[req.k] = req.v; + send next_(this), ePropagateWrite, (source = req.source, k = req.k, v = req.v); + } + } +} + + +machine Tail { + var kv: map[int, int]; + + start state Replying { + on ePropagateWrite do (req: tWriteRequest) { + kv[req.k] = req.v; + send req.source, eWriteResponse, (source = req.source, k = req.k, v = req.v); + } + + on eReadRequest do (req: tReadRequest) { + if (req.k in kv) { + send req.source, eReadResponse, (source = req.source, k = req.k, v = kv[req.k], status = true); + } else { + send req.source, eReadResponse, (source = req.source, k = req.k, v = -1, status = false); + } + } + } +} + +machine Client { + start state Loop { + entry { + var k: int; + var v: int; + + k = RandomInt(); + + if ($) { + v = RandomInt(); + send head(), eWriteRequest, (source = this, k = k, v = v); + } else { + send tail(), eReadRequest, (source = this, k = k); + } + + goto Loop; + } + ignore eWriteResponse, eReadResponse; // not actually doing anything with these in the client + } +} + +fun RandomInt(): int; + +spec StrongConsistency observes eReadResponse, eWriteResponse { + var kv : map[int, int]; + start state WaitForEvents { + on eWriteResponse do (resp: tWriteRequest) { + kv[resp.k] = resp.v; + } + on eReadResponse do (resp: tReadResponse) { + if (resp.k in kv) { + assert resp.status == true; + assert resp.v == kv[resp.k]; + } else { + assert resp.status == false; + } + } + } +} + +// begin proof +pure head(): machine; +pure tail(): machine; +pure next_(m: machine): machine; + +// set all the fields to their default values +init-condition forall (p: Head) :: p.kv == default(map[int, int]); +init-condition forall (p: Body) :: p.kv == default(map[int, int]); +init-condition forall (p: Tail) :: p.kv == default(map[int, int]); +init-condition StrongConsistency.kv == default(map[int, int]); + +// assume the pure functions match the state at the start +init-condition forall (m: machine) :: m == head() == m is Head; +init-condition forall (m: machine) :: m == tail() == m is Tail; +init-condition forall (m: machine) :: next_(m) is Body || next_(m) is Tail; +// ensure that the pure functions continue to match the state as time goes on +invariant next_1: forall (m: machine) :: m == head() == m is Head; +invariant next_2: forall (m: machine) :: m == tail() == m is Tail; +invariant next_3: forall (m: machine) :: next_(m) is Body || next_(m) is Tail; + +// Aux invariants for P obligations +invariant only_head_receives_writes: forall (m: machine, e: event) :: (inflight e && e is eWriteRequest && e targets m) ==> (m is Head); +invariant only_tail_receives_reads: forall (m: machine, e: event) :: (inflight e && e is eReadRequest && e targets m) ==> (m is Tail); +invariant only_client_receives_read_response: forall (m: machine, e: event) :: (inflight e && e is eReadResponse && e targets m) ==> (m is Client); +invariant only_client_receives_write_response: forall (m: machine, e: event) :: (inflight e && e is eWriteResponse && e targets m) ==> (m is Client); +invariant only_body_or_tail_receive_props: forall (m: machine, e: event) :: (inflight e && e is ePropagateWrite && e targets m) ==> (m is Tail || m is Body); +invariant source_is_always_client_1: forall (e: eWriteRequest) :: inflight e ==> e.source is Client; +invariant source_is_always_client_2: forall (e: eReadRequest) :: inflight e ==> e.source is Client; +invariant source_is_always_client_3: forall (e: ePropagateWrite) :: inflight e ==> e.source is Client; +invariant source_is_always_client_4: forall (e: eReadResponse) :: inflight e ==> e.source is Client; +invariant source_is_always_client_5: forall (e: eWriteResponse) :: inflight e ==> e.source is Client; + +// Aux invariant for spec machine +invariant tail_sync: forall (t: Tail) :: t.kv == StrongConsistency.kv; diff --git a/Tutorial/Advanced/1_ChainReplicationVerification/portfolio-config.json b/Tutorial/Advanced/1_ChainReplicationVerification/portfolio-config.json new file mode 100644 index 0000000000..f911404168 --- /dev/null +++ b/Tutorial/Advanced/1_ChainReplicationVerification/portfolio-config.json @@ -0,0 +1,7 @@ +{ + "pproj": { + "help" : "Name of the .pproj file in the project directory", + "default" : "ChainReplicationVerification.pproj", + "metavar" : "F" + } +} diff --git a/Tutorial/Advanced/2_TwoPhaseCommitVerification/.gitignore b/Tutorial/Advanced/2_TwoPhaseCommitVerification/.gitignore new file mode 100644 index 0000000000..161a65f6d8 --- /dev/null +++ b/Tutorial/Advanced/2_TwoPhaseCommitVerification/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tutorial/Advanced/2_TwoPhaseCommitVerification/KeyValue/PSrc/System.p b/Tutorial/Advanced/2_TwoPhaseCommitVerification/KeyValue/PSrc/System.p new file mode 100644 index 0000000000..1d83cc139e --- /dev/null +++ b/Tutorial/Advanced/2_TwoPhaseCommitVerification/KeyValue/PSrc/System.p @@ -0,0 +1,246 @@ +/********************************************************* +Clients send read and write requests to a coordinator. On write requests, the coordinator does a two phase commit with +all participants. On read requests, the coordinator just asks a random participant to respond to the client. + +All participants must agree on every commited write. The monitor keeps track of all write responses, which is the ground +truth for what is commited. Every participant must be maintaining a subset of this. +**********************************************************/ + +enum tVote {YES, NO} + +type tRound = int; +type tKey = int; +type tValue = int; + +type rvPair = (round: tRound, value: tValue); +type krvTriple = (key: tKey, round: tRound, value: tValue); + +type tVoteResp = (origin: machine, triple: krvTriple, vote: tVote, source: machine); +type tVoteReq = (origin: machine, triple: krvTriple); +type tWriteReq = (origin: machine, key: tKey, value: tValue); +type tReadReq = (origin: machine, key: tKey); +type tWriteResp = (triple: krvTriple, vote: tVote); +type tReadResp = (key: tKey, versions: set[rvPair], source: machine); + +event eVoteReq : tVoteReq; +event eVoteResp: tVoteResp; +event eAbort : tVoteReq; +event eCommit : tVoteReq; + +event eWriteReq : tWriteReq; +event eWriteResp: tWriteResp; +event eReadReq : tReadReq; +event eReadResp : tReadResp; + +fun RandomInt(): int; +fun RandomParticipant(s: set[machine]) + return (x: machine); + ensures x in s; + +machine Client { + start state Loop { + entry { + var k: int; + var v: int; + + k = RandomInt(); + v = RandomInt(); + + if ($) { + v = RandomInt(); + send coordinator(), eWriteReq, (origin = this, key = k, value = v); + } else { + send coordinator(), eReadReq, (origin = this, key = k); + } + + goto Loop; + } + ignore eWriteResp, eReadResp; + } +} + +machine Coordinator +{ + var yesVotes: map[krvTriple, set[machine]]; + var commited: set[krvTriple]; + var aborted : set[krvTriple]; + + start state Serving { + on eReadReq do (req: tReadReq) { + var p: machine; + p = RandomParticipant(participants()); + send p, eReadReq, req; + } + + on eWriteReq do (req: tWriteReq) { + var p: machine; + var r: tRound; + assume (forall (t: krvTriple) :: t in yesVotes ==> t.round != r); + + yesVotes[(key = req.key, round = r, value = req.value)] = default(set[machine]); + + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eVoteReq; + invariant forall new (e: eVoteReq) :: e.triple.round == r && e.triple.key == req.key && e.triple.value == req.value && e.origin == req.origin; + { + send p, eVoteReq, (origin = req.origin, triple = (key = req.key, round = r, value = req.value)); + } + } + + on eVoteResp do (resp: tVoteResp) { + var p: machine; + + if (resp.vote == YES) { + yesVotes[resp.triple] += (resp.source); + + if (yesVotes[resp.triple] == participants()) { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eCommit; + invariant forall new (e: eCommit) :: e.triple == resp.triple && e.origin == resp.origin; + { + send p, eCommit, (origin = resp.origin, triple = resp.triple); + } + + commited += (resp.triple); + send resp.origin, eWriteResp, (triple = resp.triple, vote = resp.vote); + goto Serving; + } + + } else { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eAbort; + invariant forall new (e: eAbort) :: e.triple == resp.triple && e.origin == resp.origin; + { + send p, eAbort, (origin = resp.origin, triple = resp.triple); + } + + aborted += (resp.triple); + send resp.origin, eWriteResp, (triple = resp.triple, vote = resp.vote); + goto Serving; + } + } + } +} + +machine Participant { + var commited: set[krvTriple]; + var aborted: set[krvTriple]; + var kv: map[tKey, set[rvPair]]; + + start state Acting { + on eVoteReq do (req: tVoteReq) { + send coordinator(), eVoteResp, (origin = req.origin, triple = req.triple, vote = preference(this, req.triple), source = this); + } + + on eCommit do (req: tVoteReq) { + commited += (req.triple); + if (!(req.triple.key in kv)) { + kv[req.triple.key] = default(set[rvPair]); + } + kv[req.triple.key] += ((round = req.triple.round, value = req.triple.value)); + } + + on eAbort do (req: tVoteReq) { + aborted += (req.triple); + } + + on eReadReq do (req: tReadReq) { + if (req.key in kv) { + send req.origin, eReadResp, (key = req.key, versions = kv[req.key], source = this); + } else { + send req.origin, eReadResp, (key = req.key, versions = default(set[rvPair]), source = this); + } + } + } +} + +spec Consistency observes eReadResp, eWriteResp { + var kv: map[tKey, set[rvPair]]; + start state WaitForEvents { + on eWriteResp do (resp: tWriteResp) { + if (resp.vote == YES) { + kv[resp.triple.key] += ((round = resp.triple.round, value = resp.triple.value)); + } + } + on eReadResp do (resp: tReadResp) { + // Everything we send back was actually written. + assert subset(resp.versions, kv[resp.key]); + // Everyone agrees on what we send back + assert (forall (t: krvTriple) :: (resp.key == t.key && (round = t.round, value = t.value) in resp.versions) ==> (forall (p: Participant) :: preference(p, t) == YES)); + } + } +} + +// using these to avoid initialization +pure participants(): set[machine]; +pure coordinator(): machine; +pure preference(m: machine, triple: krvTriple) : tVote; + +pure subset(small: set[rvPair], large: set[rvPair]) : bool = forall (rv: rvPair) :: rv in small ==> rv in large; + +// lets assume that there is at least one participant +axiom exists (x: machine) :: x in participants(); + +// assumptions about how the system is setup and the pure functions above +init-condition coordinator() is Coordinator; +init-condition forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2; +init-condition forall (m: machine) :: m in participants() == m is Participant; + +// making sure that our assumptions about pure functions are not pulled out from underneath us +invariant c_is_coordinator: coordinator() is Coordinator; +invariant one_coordinator: forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2; +invariant participant_set: forall (m: machine) :: m in participants() == m is Participant; + +// set all the fields to their default values +init-condition forall (c: Coordinator) :: c.yesVotes == default(map[krvTriple, set[machine]]); +init-condition forall (c: Coordinator) :: c.commited == default(set[krvTriple]); +init-condition forall (c: Coordinator) :: c.aborted == default(set[krvTriple]); +init-condition forall (p: Participant) :: p.commited == default(set[krvTriple]); +init-condition forall (p: Participant) :: p.aborted == default(set[krvTriple]); +init-condition forall (p: Participant) :: p.kv == default(map[tKey, set[rvPair]]); +init-condition Consistency.kv == default(map[tKey, set[rvPair]]); + +// make sure we never get a message that we're not expecting +invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; +invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; +invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; +invariant never_resp_to_participant: forall (e: event, p: Participant) :: e is eVoteResp && e targets p ==> !inflight e; +invariant never_writeReq_to_participant: forall (e: event, p: Participant) :: e is eWriteReq && e targets p ==> !inflight e; +invariant never_writeResp_to_participant: forall (e: event, p: Participant) :: e is eWriteResp && e targets p ==> !inflight e; +invariant never_readResp_to_participant: forall (e: event, p: Participant) :: e is eReadResp && e targets p ==> !inflight e; +invariant never_writeResp_to_coordinator: forall (e: event, c: Coordinator) :: e is eWriteResp && e targets c ==> !inflight e; +invariant never_readResp_to_coordinator: forall (e: event, c: Coordinator) :: e is eReadResp && e targets c ==> !inflight e; +invariant never_voteReq_to_client: forall (e: event, c: Client) :: e is eVoteReq && e targets c ==> !inflight e; +invariant never_voteResp_to_client: forall (e: event, c: Client) :: e is eVoteResp && e targets c ==> !inflight e; +invariant never_abort_to_client: forall (e: event, c: Client) :: e is eAbort && e targets c ==> !inflight e; +invariant never_commit_to_client: forall (e: event, c: Client) :: e is eCommit && e targets c ==> !inflight e; +invariant never_writeReq_to_client: forall (e: event, c: Client) :: e is eWriteReq && e targets c ==> !inflight e; +invariant never_readReq_to_client: forall (e: event, c: Client) :: e is eReadReq && e targets c ==> !inflight e; +invariant readReq_origin_is_client: forall (e: eReadReq) :: inflight e ==> e.origin is Client; +invariant writeReq_origin_is_client: forall (e: eWriteReq) :: inflight e ==> e.origin is Client; +invariant voteReq_origin_is_client: forall (e: eVoteReq) :: inflight e ==> e.origin is Client; +invariant voteResp_origin_is_client: forall (e: eVoteResp) :: inflight e ==> e.origin is Client; + +// aux invariants for consistency monitor first assertion +invariant p_subset_monitor_kv: forall (p: Participant, k: tKey) :: k in p.kv ==> subset(p.kv[k], Consistency.kv[k]); +invariant c_commited_means_in_monitor_kv: forall (c: Coordinator, t: krvTriple) :: t in c.commited ==> ((round = t.round, value = t.value) in Consistency.kv[t.key]); + +// aux invariants for consistency monitor second assertion +// essentially the 2pc property, but restated for kv elements +invariant in_kv_means_all_preferred: forall (p1: Participant, t: krvTriple) :: (t.key in p1.kv && (round = t.round, value = t.value) in p1.kv[t.key]) ==> (forall (p2: Participant) :: preference(p2, t) == YES); + +// supporting invariants for the 2pc property +invariant a1: forall (e: eVoteResp) :: sent e ==> e.source is Participant; +invariant a2: forall (e: eVoteResp) :: sent e ==> e.vote == preference(e.source, e.triple); +invariant a3a: forall (c: Coordinator, e: eCommit) :: sent e ==> e.triple in c.commited; +invariant a3b: forall (c: Coordinator, e: eAbort) :: sent e ==> e.triple in c.aborted; +invariant a4: forall (c: Coordinator, t: krvTriple, p1: Participant) :: t in p1.commited ==> t in c.commited; +invariant a5: forall (p: Participant, c: Coordinator, t: krvTriple) :: (t in c.yesVotes && p in c.yesVotes[t]) ==> preference(p, t) == YES; +invariant a6: forall (c: Coordinator, t: krvTriple) :: t in c.commited ==> (forall (p2: Participant) :: preference(p2, t) == YES); +invariant a7a: forall (c: Coordinator, e: eVoteReq) :: sent e ==> e.triple in c.yesVotes; +invariant a7b: forall (c: Coordinator, e: eVoteResp) :: sent e ==> e.triple in c.yesVotes; + + diff --git a/Tutorial/Advanced/2_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj b/Tutorial/Advanced/2_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj new file mode 100644 index 0000000000..f76aad3a17 --- /dev/null +++ b/Tutorial/Advanced/2_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj @@ -0,0 +1,8 @@ + +TwoPhaseCommitVerification + + ./PSrc/ + +./PGenerated/ +PVerifier + diff --git a/Tutorial/Advanced/2_TwoPhaseCommitVerification/Rounds/PSrc/System.p b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Rounds/PSrc/System.p new file mode 100644 index 0000000000..d321afe444 --- /dev/null +++ b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Rounds/PSrc/System.p @@ -0,0 +1,136 @@ +enum Vote {YES, NO} +type Round = int; +type tVoteResp = (source: machine, round: Round, vote: Vote); +type tVoteReq = (round: Round); + +event eVoteReq: tVoteReq; +event eVoteResp: tVoteResp; +event eAbort: tVoteReq; +event eCommit: tVoteReq; + +machine Coordinator +{ + var yesVotes: map[Round, set[machine]]; + var commited: set[Round]; + var aborted: set[Round]; + + start state Init { + entry { + var p: machine; + var r: Round; + assume !(r in yesVotes); + + yesVotes[r] = default(set[machine]); + + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eVoteReq; + invariant forall new (e: eVoteReq) :: e.round == r; + { + send p, eVoteReq, (round = r,); + } + + goto WaitForResponses; + } + + defer eVoteResp; + } + + state WaitForResponses { + on eVoteResp do (resp: tVoteResp) { + var p: machine; + + if (resp.vote == YES) { + yesVotes[resp.round] += (resp.source); + + if (yesVotes[resp.round] == participants()) { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eCommit; + invariant forall new (e: eCommit) :: e.round == resp.round; + { + send p, eCommit, (round = resp.round,); + } + + commited += (resp.round); + goto Init; + } + + } else { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eAbort; + invariant forall new (e: eAbort) :: e.round == resp.round; + { + send p, eAbort, (round = resp.round,); + } + + aborted += (resp.round); + goto Init; + } + } + } +} + +machine Participant { + var commited: set[Round]; + var aborted: set[Round]; + + start state Undecided { + on eVoteReq do (req: tVoteReq) { + send coordinator(), eVoteResp, (source = this, round = req.round, vote = preference(this, req.round)); + } + + on eCommit do (req: tVoteReq) { + commited += (req.round); + } + + on eAbort do (req: tVoteReq) { + aborted += (req.round); + } + } +} + +// using these to avoid initialization +pure participants(): set[machine]; +pure coordinator(): machine; +pure preference(m: machine, r: Round) : Vote; + +// assumptions about how the system is setup and the pure functions above +init-condition forall (m: machine) :: m == coordinator() == m is Coordinator; +init-condition forall (m: machine) :: m in participants() == m is Participant; + +// making sure that our assumptions about pure functions are not pulled out from underneath us +invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator; +invariant participant_set: forall (m: machine) :: m in participants() == m is Participant; + +// set all the fields to their default values +init-condition forall (c: Coordinator) :: c.yesVotes == default(map[Round, set[machine]]); +init-condition forall (c: Coordinator) :: c.commited == default(set[Round]); +init-condition forall (c: Coordinator) :: c.aborted == default(set[Round]); +init-condition forall (p: Participant) :: p.commited == default(set[Round]); +init-condition forall (p: Participant) :: p.aborted == default(set[Round]); + +// make sure we never get a message that we're not expecting +invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; +invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; +invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; +invariant never_resp_to_participant: forall (e: event, p: Participant) :: e is eVoteResp && e targets p ==> !inflight e; + +// the main invariant we care about +invariant safety: forall (c: Coordinator, p1: Participant, r: Round) :: (r in p1.commited ==> (forall (p2: Participant) :: preference(p2, r) == YES)); + +// supporting invariants from non-round proof +invariant a1: forall (e: eVoteResp) :: sent e ==> e.source is Participant; +invariant a2: forall (e: eVoteResp) :: sent e ==> e.vote == preference(e.source, e.round); +invariant a3a: forall (c: Coordinator, e: eCommit) :: sent e ==> e.round in c.commited; +invariant a3b: forall (c: Coordinator, e: eAbort) :: sent e ==> e.round in c.aborted; +invariant a4: forall (c: Coordinator, r: Round, p1: Participant) :: r in p1.commited ==> r in c.commited; +invariant a5: forall (p: Participant, c: Coordinator, r: Round) :: (r in c.yesVotes && p in c.yesVotes[r]) ==> preference(p, r) == YES; +invariant a6: forall (c: Coordinator, r: Round) :: r in c.commited ==> (forall (p2: Participant) :: preference(p2, r) == YES); + +// make sure that votes have been initialized +invariant a7a: forall (c: Coordinator, e: eVoteReq) :: sent e ==> e.round in c.yesVotes; +invariant a7b: forall (c: Coordinator, e: eVoteResp) :: sent e ==> e.round in c.yesVotes; + + diff --git a/Tutorial/Advanced/2_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj new file mode 100644 index 0000000000..f76aad3a17 --- /dev/null +++ b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj @@ -0,0 +1,8 @@ + +TwoPhaseCommitVerification + + ./PSrc/ + +./PGenerated/ +PVerifier + diff --git a/Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/PSrc/System.p b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/PSrc/System.p new file mode 100644 index 0000000000..811372b77d --- /dev/null +++ b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/PSrc/System.p @@ -0,0 +1,126 @@ +type tVoteResp = (source: machine); + +event eVoteReq; +event eYes: tVoteResp; +event eNo: tVoteResp; +event eAbort; +event eCommit; + +machine Coordinator +{ + var yesVotes: set[machine]; + + start state Init { + entry { + var p: machine; + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eVoteReq; + { + send p, eVoteReq; + } + goto WaitForResponses; + } + } + + state WaitForResponses { + on eYes do (resp: tVoteResp) { + var p: machine; + yesVotes += (resp.source); + if (yesVotes == participants()) { + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eCommit; + { + send p, eCommit; + } + goto Committed; + } + } + on eNo do (resp: tVoteResp) { + var p: machine; + foreach (p in participants()) + invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants(); + invariant forall new (e: event) :: e is eAbort; + { + send p, eAbort; + } + goto Aborted; + } + } + + state Committed {ignore eYes, eNo;} + state Aborted {ignore eYes, eNo;} +} + +machine Participant { + start state Undecided { + on eVoteReq do { + if (preference(this)) { + send coordinator(), eYes, (source = this,); + } else { + send coordinator(), eNo, (source = this,); + } + } + + on eCommit do { + goto Accepted; + } + + on eAbort do { + goto Rejected; + } + } + + state Accepted {ignore eVoteReq, eCommit, eAbort;} + state Rejected {ignore eVoteReq, eCommit, eAbort;} +} + +// using these to avoid initialization +pure participants(): set[machine]; +pure coordinator(): machine; +pure preference(m: machine) : bool; + +// assumptions about how the system is setup and the pure functions above +init-condition forall (m: machine) :: m == coordinator() == m is Coordinator; +init-condition forall (m: machine) :: m in participants() == m is Participant; + +// set all the fields to their default values +init-condition forall (c: Coordinator) :: c.yesVotes == default(set[machine]); + +// making sure that our assumptions about pure functions are not pulled out from underneath us +Lemma system_config { + invariant one_coordinator: forall (m: machine) :: m == coordinator() <==> m is Coordinator; + invariant participant_set: forall (m: machine) :: m in participants() <==> m is Participant; + invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e; + invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e; + invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e; + invariant never_yes_to_participant: forall (e: event, p: Participant) :: e is eYes && e targets p ==> !inflight e; + invariant never_yes_to_init: forall (e: event, c: Coordinator) :: e is eYes && e targets c && c is Init ==> !inflight e; + invariant never_no_to_participant: forall (e: event, p: Participant) :: e is eNo && e targets p ==> !inflight e; + invariant never_no_to_init: forall (e: event, c: Coordinator) :: e is eNo && e targets c && c is Init ==> !inflight e; + invariant req_implies_not_init: forall (e: event, c: Coordinator) :: e is eVoteReq && c is Init ==> !inflight e; +} + +// the main invariant we care about +invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2)); + +// supporting invariants, based on the Kondo paper +Lemma kondo { + invariant a1a: forall (e: eYes) :: inflight e ==> e.source in participants(); + invariant a1b: forall (e: eNo) :: inflight e ==> e.source in participants(); + invariant a2a: forall (e: eYes) :: inflight e ==> preference(e.source); + invariant a2b: forall (e: eNo) :: inflight e ==> !preference(e.source); + invariant a3b: forall (e: eAbort) :: inflight e ==> coordinator() is Aborted; + invariant a3a: forall (e: eCommit) :: inflight e ==> coordinator() is Committed; + invariant a4: forall (p: Participant) :: p is Accepted ==> coordinator() is Committed; + invariant a5: forall (p: Participant, c: Coordinator) :: p in c.yesVotes ==> preference(p); + invariant a6: coordinator() is Committed ==> (forall (p: Participant) :: p in participants() ==> preference(p)); +} + +Proof { + prove system_config; + prove kondo using system_config; + prove safety using kondo; + prove default using system_config; +} \ No newline at end of file diff --git a/Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj new file mode 100644 index 0000000000..f76aad3a17 --- /dev/null +++ b/Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj @@ -0,0 +1,8 @@ + +TwoPhaseCommitVerification + + ./PSrc/ + +./PGenerated/ +PVerifier + diff --git a/Tutorial/Advanced/3_RingLeaderVerification/.gitignore b/Tutorial/Advanced/3_RingLeaderVerification/.gitignore new file mode 100644 index 0000000000..161a65f6d8 --- /dev/null +++ b/Tutorial/Advanced/3_RingLeaderVerification/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tutorial/Advanced/3_RingLeaderVerification/PSrc/System.p b/Tutorial/Advanced/3_RingLeaderVerification/PSrc/System.p new file mode 100644 index 0000000000..9779f81000 --- /dev/null +++ b/Tutorial/Advanced/3_RingLeaderVerification/PSrc/System.p @@ -0,0 +1,47 @@ +type tNominate = (voteFor: machine); + +event eNominate : tNominate; + +pure le(x: machine, y: machine): bool; +axiom forall (x: machine) :: le(x, x); +axiom forall (x: machine, y: machine) :: le(x, y) || le(y, x); +axiom forall (x: machine, y: machine, z: machine) :: (le(x, y) && le(y, z)) ==> le(x, z); +axiom forall (x: machine, y: machine) :: (le(x, y) && le(y, x)) ==> (x == y); + +pure btw(x: machine, y: machine, z: machine): bool; +axiom forall (w: machine, x: machine, y: machine, z: machine) :: (btw(w, x, y) && btw(w, y, z)) ==> btw(w, x, z); +axiom forall (x: machine, y: machine, z: machine) :: btw(x, y, z) ==> !btw(x, z, y); +axiom forall (x: machine, y: machine, z: machine) :: btw(x, y, z) || btw(x, z, y) || (x == y) || (x == z) || (y == z); +axiom forall (x: machine, y: machine, z: machine) :: btw(x, y, z) ==> btw(y, z, x); + +pure right(x: machine): machine; +axiom forall (x: machine) :: x != right(x); +axiom forall (x: machine, y: machine) :: (x != y && y != right(x)) ==> btw(x, right(x), y); + +machine Server { + start state Proposing { + entry { + send right(this), eNominate, (voteFor=this,); + } + on eNominate do (n: tNominate) { + if (n.voteFor == this) { + goto Won; + } else if (le(this, n.voteFor)) { + send right(this), eNominate, (voteFor=n.voteFor,); + } else { + send right(this), eNominate, (voteFor=this,); + } + } + } + state Won { + ignore eNominate; + } +} + +// voteFor is the running max +invariant NoBypass: forall (n: machine, m: machine, e: eNominate) :: (inflight e && e targets m && n is Server && btw(e.voteFor, n, m)) ==> le(n, e.voteFor); +invariant SelfPendingMax: forall (n: machine, m: machine, e: eNominate) :: (inflight e && e targets m && e.voteFor == m) ==> le(n, m); + +// Main theorems +invariant LeaderMax: forall (x: machine, y: machine) :: x is Won ==> le(y, x); +invariant UniqueLeader: forall (x: machine, y: machine) :: (x is Won && y is Won) ==> (le(x, y) && le(y, x)); \ No newline at end of file diff --git a/Tutorial/Advanced/3_RingLeaderVerification/RingLeaderVerification.pproj b/Tutorial/Advanced/3_RingLeaderVerification/RingLeaderVerification.pproj new file mode 100644 index 0000000000..b121122658 --- /dev/null +++ b/Tutorial/Advanced/3_RingLeaderVerification/RingLeaderVerification.pproj @@ -0,0 +1,8 @@ + +RingLeaderVerification + + ./PSrc/ + +./PGenerated/ +PVerifier +