Start to move PVerifier so that its ready to be merged into P3.0 (#805)

* Prototype Support For Verification (#762) * Initial commit for UCLID5 backend. Mostly type definitions for now. * Start encoding of handlers and statements. Need to encode expressions. * small update to assignment handling and generate comments to see what is missing * add next block * support more statements and expressions * refactor before adding helper functions to shorten explicit strings * use more macros so that updates are consistent. Also, use local variables in procedures and then bundle up the new machine using these local variables at the end of the procedure. * WIP: UCLID reserved words, like input, need to be taken care of when printing. * switch from enums for state to datatypes * fix bug in skipping handlers; use .States consistently. WIP: need to support map types correctly * Update UCLID5 backend: avoid keywords through prefix scheme * add support for maps * Functions are procedures; implement call site; need to generate procedure code. * add support for helper function bodies as UCLID procedures. Always call a procedure with an argument representing the calling machine. * add simple chain replication and update compiler to handle it * add helper for setting field defaults for maps and sets; init fields to defaults * fix bug in precodnition for event handlers * add happy path chain replication * add ucl files * checkpoint chain replication * add support for foreach statements, default expressions, etc, before moving to new encoding * add goto types * add label type * gotos should carry target. Need to redo procedures and next block to handle labels. * WIP: rewrite UCLID5 backend to use labels and not have implicit ignores. Need to add handlers back in. * Finish foundation of new encoding * inline deref function * WIP: add support for spec machines. Now constructing listener map, need to use map on sends. * add spec procedure calls after evry send * WIP: add invariant to parser * add support for invariants at the P level * add support for quantifier expressions * add support for quantifying over machines * fix bugs in permission type quantification * add support for pure, a keyword for specification functions. Need to fix TestExpr * add enough proof syntax to prove that clients in chain rep don't receive unexpected events * add 9, fix compiler bug for empty events, start proof * add axiom keyword * add support for testing state * incorrect proof. Need to find contradiction * make sure to verify all procedurs * add support for quantifying over and selecting from specific event kinds * add partial 2pc proof. Need to add syntax for talking about state delay * add compiler pass to uclid backend * add difference constraints * full 2pc proof * deal with final proof obligation of 2pc * add simple chain replication verification, add spec machine field access, change flying to inflight * add unique identifier to actions and automatically prove that it is actually unique * add sent keyword * remove stale examples. Will add back later when updated. * rename tutorial * add support for limited map nesting; start adding multi round 2pc * start adding support for choose (placeholder); add support for assume * update 2pc rounds with assumption; add ring leader election that needs a bit more time to solve than the default * add limited support for choose expressions * add support for pure functions with bodies * better verification feedback for users * add timeout for UCLID5 backend * allow for specific events in diff loop invaraints * start generalizing 2pc with rounds * finish 2pc rounds; fix bug with negative timeout value * reorganize verification tutorial * add feedback for failing to prove assertions and update 2pc kv example to show it off * add kv version of 2pc that has a consistency monitor * make users init fields to default values * fix bug when spec machine handlers don't take arguments * add support for return statements (although we are not actually exiting the procedure on them) * fix bug in global procedure bindings; inline procedures unless they do not have a body. * handle empty payloads for spec handlers * add parens around state check to avoid binding issues; update 2pc-key-value example to generate random values too * [fix] canonicalize container type before checking for codegen * add 'handles-all' flag that can be turned off to avoid checking that all events are handled * add support for iterating over maps with the keys expression * more missing parens * add check-only argument and change no-event-handler-checks to a flag * fix bugs in new command line options * no need to run any handlers in next block. Fix condition for check only flag. * don't forget to check the base case! * relax type checking on pure functions * do not init local variables to default values * add missing local variable declarations for global procedures --------- Co-authored-by: AD1024 <[email protected]> Co-authored-by: Ankush Desai <[email protected]> * add install instructions for amazon linux * [Feature] `prove * using *` command for incremental proof construction (#783) * [add] prove using command * [add] invariant ref * [save] generating queries for proof commands * [save] finish commands * save parallization * save * save * save * save * [save] more tweaks * remove some commented code * [fix] separate sanity check and event handler checks * [add] `except` keyword * remove some commented code * [fix] generate local state for spec machines * add support for foreign functions with contracts and update one tutorial to include an example * allow duplicate invariant names in different groups using group name as prefix * add caching using liteDB and md5 hash of uclid files * fix bug in caching by simplifying process checklist * fix bug in global procedures: always prepend self reference * add default that captures P's proof obligations * fix bug in file names * cleanup example for tutorial * add 2pc verification tutorial * pverifier backend and reorganize verification tutorials * init keyword -> init-condition keyword * add error message when trying to use pverifier syntax for other backends * move install instructions to docs and update link in 2pc verification tutorial. * rename uclid5 backend to pverifier * remove unnecessary imports * add iff symbol --------- Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]>
p-org · Dec 10, 2024 · 98c6ddf · 98c6ddf
1 parent 65042fe
commit 98c6ddf
Show file tree

Hide file tree

Showing 68 changed files with 4,778 additions and 57 deletions.
diff --git a/Docs/docs/advanced/install-verification-backend.md 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
+```
diff --git a/Docs/docs/tutorial/advanced/twophasecommitverification.md b/Docs/docs/tutorial/advanced/twophasecommitverification.md
diff --git 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
@@ -364,6 +364,22 @@ private List<IPStmt> SimplifyStatement(IPStmt statement)
                         }).ToList()));
                     return assertDeps.Concat(new List<IPStmt>{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<IPStmt>{aifStmtForAssert})
+                        .ToList();
 
                 case AssignStmt assignStmt:
                     (var assignLV, var assignLVDeps) = SimplifyLvalue(assignStmt.Location);
@@ -434,7 +450,6 @@ private List<IPStmt> 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
@@ -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; }
+}