From 74999b4ba98ad1ef0c3232c445aab18416260d24 Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Fri, 1 Nov 2024 18:22:07 -0700 Subject: [PATCH] add default that captures P's proof obligations --- .../Backend/Uclid5/Uclid5CodeGenerator.cs | 84 ++++++++++++++----- Src/PCompiler/CompilerCore/Parser/PParser.g4 | 2 +- .../TypeChecker/AST/Declarations/Invariant.cs | 10 +++ .../TypeChecker/DeclarationStubVisitor.cs | 4 +- .../TypeChecker/DeclarationVisitor.cs | 10 ++- .../KeyValue/PSrc/System.p | 3 + .../Single_Incremental/PSrc/System.p | 7 +- 7 files changed, 91 insertions(+), 29 deletions(-) diff --git a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs index 39948e882c..bef11ca44d 100644 --- a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs @@ -47,6 +47,7 @@ public void Compile(ICompilerConfiguration job) 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")); @@ -62,7 +63,11 @@ public void Compile(ICompilerConfiguration job) foreach (var cmd in _commands) { - job.Output.WriteInfo($"Proof command: {cmd.Name}"); + if (cmd.Name == "default") + { + missingDefault = false; + } + job.Output.WriteInfo($"Proving: {cmd.Name}"); Dictionary checklist = _proofCommandToFiles[cmd].ToDictionary(x => x, x => false); Dictionary tasks = []; @@ -93,6 +98,9 @@ public void Compile(ICompilerConfiguration job) } } } + + var numCompleted = checklist.Values.Sum(x => x ? 1 : 0); + Console.Write($"\ršŸ” Checked {numCompleted}/{checklist.Count} goals..."); // fetch while (checklist.ContainsValue(false)) @@ -150,8 +158,8 @@ public void Compile(ICompilerConfiguration job) newTasks.ToList().ForEach(x => tasks.Add(x.Key, x.Value)); } - var numCompleted = checklist.Values.Sum(x => x ? 1 : 0); - Console.Write($"\ršŸ” Verifying {numCompleted}/{checklist.Count} goals..."); + numCompleted = checklist.Values.Sum(x => x ? 1 : 0); + Console.Write($"\ršŸ” Checked {numCompleted}/{checklist.Count} goals..."); } Console.WriteLine(); @@ -161,14 +169,18 @@ public void Compile(ICompilerConfiguration job) job.Output.WriteInfo($"\nšŸŽ‰ Verified {succeededInv.Count} invariants!"); foreach (var inv in succeededInv) { - job.Output.WriteInfo($"āœ… {inv.Name}"); + job.Output.WriteInfo($"āœ… {inv.Name.Replace("_PGROUP_", ": ")}"); + } + if (!missingDefault && failMessages.Count == 0) + { + job.Output.WriteInfo($"āœ… default P proof obligations"); } MarkProvenInvariants(succeededInv); - ShowRemainings(job, failedInv); + ShowRemainings(job, failedInv, missingDefault); if (failMessages.Count > 0) { - job.Output.WriteInfo($"āŒ Failed to verify {failMessages.Count} invariants!"); + job.Output.WriteInfo($"āŒ Failed to verify {failMessages.Count} properties!"); foreach (var msg in failMessages) { job.Output.WriteError(msg); @@ -195,7 +207,7 @@ private void MarkProvenInvariants(HashSet succeededInv) } } - private void ShowRemainings(ICompilerConfiguration job, HashSet failedInv) + private void ShowRemainings(ICompilerConfiguration job, HashSet failedInv, bool missingDefault) { HashSet remaining = []; foreach (var inv in _provenInvariants) @@ -209,12 +221,17 @@ private void ShowRemainings(ICompilerConfiguration job, HashSet faile } } - if (remaining.Count > 0) + if (remaining.Count > 0 || missingDefault) { job.Output.WriteWarning("ā“ Remaining Goals:"); foreach (var inv in remaining) { - job.Output.WriteWarning($"- {inv.Name} at {GetLocation(inv)}"); + job.Output.WriteWarning($"- {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(inv)}"); + } + + if (missingDefault) + { + job.Output.WriteWarning($"- default P proof obligations"); } } } @@ -229,7 +246,7 @@ private void ProcessFailureMessages(List collection, string[] query, stri 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; + var invName = matchName.Groups[1].Value.Replace("_PGROUP_", ": "); failedInv.Add(invName); failMessages.Add($"{reason} {line.Split("//").Last()} {step}"); } @@ -281,7 +298,7 @@ public IEnumerable GenerateCode(ICompilerConfiguration job, Scope _commands = []; _globalScope = globalScope; BuildDependencies(globalScope); - var filename_prefix = $"{job.ProjectName}_"; + var filenamePrefix = $"{job.ProjectName}_"; List files = []; if (!globalScope.ProofCommands.Any()) { @@ -292,15 +309,29 @@ public IEnumerable GenerateCode(ICompilerConfiguration job, Scope }; _commands.Add(proof); _proofCommandToFiles.Add(proof, []); - files.AddRange(CompileToFile($"{filename_prefix}default", proof, true)); + files.AddRange(CompileToFile($"{filenamePrefix}default", proof, true, true, false)); } else { foreach (var proofCmd in globalScope.ProofCommands) { - _proofCommandToFiles.Add(proofCmd, []); - files.AddRange(CompileToFile($"{filename_prefix}{proofCmd.Name}", proofCmd, true, false)); - _commands.Add(proofCmd); + if (proofCmd.Goals.Count == 1 && proofCmd.Goals[0].IsDefault) + { + var proof = new ProofCommand("default", null) + { + Goals = [], + Premises = proofCmd.Premises + }; + _commands.Add(proof); + _proofCommandToFiles.Add(proof, []); + files.AddRange(CompileToFile($"{filenamePrefix}default", proof, true, true, true)); + } + else + { + _proofCommandToFiles.Add(proofCmd, []); + files.AddRange(CompileToFile($"{filenamePrefix}{proofCmd.Name}", proofCmd, true, false, false)); + _commands.Add(proofCmd); + } } } @@ -325,7 +356,7 @@ private CompiledFile GenerateCompiledFile(ProofCommand cmd, string name, Machine return file; } - private List CompileToFile(string name, ProofCommand cmd, bool sanityCheck, bool handlerCheck = true) + 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(); @@ -340,7 +371,7 @@ private List CompileToFile(string name, ProofCommand cmd, bool san { _src = GenerateCompiledFile(cmd, name, m, s, null); files.Add(_src); - GenerateMain(m, s, null, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck); + 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))) @@ -349,7 +380,7 @@ private List CompileToFile(string name, ProofCommand cmd, bool san { _src = GenerateCompiledFile(cmd, name, m, s, e); files.Add(_src); - GenerateMain(m, s, e, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck); + GenerateMain(m, s, e, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck, builtin); } } } @@ -950,9 +981,15 @@ private void GenerateSpecHandlers(List specs) /******************************** * Traverse the P AST and generate the UCLID5 code using the types and helpers defined above *******************************/ - private void GenerateMain(Machine machine, State state, PEvent @event, List goals, - List requires, bool generateSanityChecks, bool handlerCheck = true) + private void + GenerateMain(Machine machine, State state, PEvent @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(); @@ -1062,9 +1099,12 @@ private void GenerateMain(Machine machine, State state, PEvent @event, List t.GetText())); var decl = CurrentScope.Put(name, context); nodesToDeclarations.Put(context, decl); return null; diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs index 85d626e589..4580086fab 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs @@ -732,14 +732,20 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context) { premises = CurrentScope.AllDecls.OfType().Select(x => (IPExpr) new InvariantRefExpr(x, context)).ToList(); } - if (context.goalsAll == null) + + 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(); @@ -748,6 +754,7 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context) { 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(); @@ -756,6 +763,7 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context) { 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(); diff --git a/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p index 6592649e08..27046cf9ed 100644 --- a/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p +++ b/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p @@ -181,6 +181,9 @@ 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 coordinator() is Coordinator; init forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2; diff --git a/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p index f477e4ec1e..ed63ebfe63 100644 --- a/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p +++ b/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p @@ -107,7 +107,7 @@ Lemma no_unexpected_messages { invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2) == YES); // supporting invariants, based on the Kondo paper -Lemma kondo_invs { +Lemma kondo { invariant a1: forall (e: eVoteResp) :: inflight e ==> e.source in participants(); invariant a2: forall (e: eVoteResp) :: inflight e ==> e.vote == preference(e.source); invariant a3b: forall (e: eAbort) :: inflight e ==> coordinator() is Aborted; @@ -118,7 +118,8 @@ Lemma kondo_invs { } Proof { - prove safety using kondo_invs; + prove safety using kondo; prove no_unexpected_messages, system_config; - prove kondo_invs using no_unexpected_messages, system_config; + prove kondo using no_unexpected_messages, system_config; + prove default using no_unexpected_messages, system_config; } \ No newline at end of file