Start to move PVerifier so that its ready to be merged into P3.0

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
+```

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;

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 });

Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs

@@ -349,6 +349,8 @@ static private IPStmt ReplaceVars(IPStmt stmt, Dictionary<Variable,Variable> 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:

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.Uclid5;
 
 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.Uclid5, new Uclid5CodeGenerator());
         }
 
         private static void RegisterCodeGenerator(CompilerOutput name, ICodeGenerator generator)

Src/PCompiler/CompilerCore/Backend/Uclid5/CompilationContext.cs

@@ -0,0 +1,11 @@
+namespace Plang.Compiler.Backend.Uclid5;
+
+internal class CompilationContext : CompilationContextBase
+{
+    public CompilationContext(ICompilerConfiguration job) : base(job)
+    {
+        FileName = $"{ProjectName}.ucl";
+    }
+
+    public string FileName { get; set; }
+}