From bf3552923124fd3b647801e8ab8b8ddd3bfebe9b Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 17 Aug 2023 15:57:07 -0700 Subject: [PATCH 01/10] Somewhat gracefully handle a solver segfault This prints an informative error when the solver segfaults, but it doesn't continue on to process the remaining goals as it ideally would. --- Source/Provers/SMTLib/SMTLibProcess.cs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 5a6211f45..b04e6a527 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -58,6 +58,7 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options) { solver = new Process(); solver.StartInfo = psi; + solver.EnableRaisingEvents = true; solver.ErrorDataReceived += SolverErrorDataReceived; solver.OutputDataReceived += SolverOutputDataReceived; solver.Exited += SolverExited; @@ -74,6 +75,14 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options) private void SolverExited(object sender, EventArgs e) { + if (options.Verbosity >= 2) { + Console.WriteLine($"[SMT-ERR-{{0}}] Solver exited with code {solver.ExitCode}."); + } + + if (solver.ExitCode != 0) { + HandleError($"Solver exited with code {solver.ExitCode}"); + } + lock (this) { while (outputReceivers.TryDequeue(out var source)) { source.SetResult(null); From d6f0961db65a8fbe1be3082bf8bc71118c3d1042 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 1 Sep 2023 16:42:41 -0700 Subject: [PATCH 02/10] Structured representation for program elements Instead of concatenating and parsing strings everywhere, this introduces a structured data type for representing the transformations on statement labels that can happen during Boogie elaboration and VC generation. It relieves clients from needing to parse the full unsat core element labels. --- Source/Core/AST/Absy.cs | 5 +- Source/Core/AST/AbsyCmd.cs | 9 +- Source/Core/AST/Program.cs | 2 +- Source/Core/ProgramElement.cs | 103 ++++++++++++++++++ Source/ExecutionEngine/ExecutionEngine.cs | 8 +- Source/Houdini/HoudiniSession.cs | 2 +- Source/Provers/SMTLib/ProverInterface.cs | 2 +- .../SMTLib/SMTLibInteractiveTheoremProver.cs | 7 +- Source/VCGeneration/ProofRun.cs | 2 +- Source/VCGeneration/Split.cs | 4 +- Source/VCGeneration/VCGen.cs | 15 ++- Source/VCGeneration/VCResult.cs | 2 +- 12 files changed, 138 insertions(+), 23 deletions(-) create mode 100644 Source/Core/ProgramElement.cs diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index b9eff070a..28c7ffd51 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -300,13 +300,14 @@ public void CopyIdFrom(IToken tok, ICarriesAttributes src) } } - public void CopyIdWithSuffixFrom(IToken tok, ICarriesAttributes src, string suffix) + public void CopyIdWithModificationsFrom(IToken tok, ICarriesAttributes src, Func modifier) { var id = src.FindStringAttribute("id"); if (id is not null) { - AddStringAttribute(tok, "id", id + suffix); + AddStringAttribute(tok, "id", modifier(id).SolverLabel); } } + } [ContractClassFor(typeof(Absy))] diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 5024bed36..990c18721 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -3852,7 +3852,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) // Do this after copying the attributes so it doesn't get overwritten if (callId is not null) { - (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires"); + (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, + id => new CallRequiresGoalElement(callId, id)); } a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; @@ -3868,7 +3869,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(a != null); // These probably won't have IDs, but copy if they do. if (callId is not null) { - (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires_assumed"); + (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, + id => new CallRequiresAssumedElement(callId, id)); } newBlockBody.Add(a); @@ -4034,7 +4036,8 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #endregion if (callId is not null) { - (assume as ICarriesAttributes).CopyIdWithSuffixFrom(tok, e, $"${callId}$ensures"); + (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e, + id => new CallEnsuresElement(callId, id)); } newBlockBody.Add(assume); diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index 82e07de3d..50d7dabb2 100644 --- a/Source/Core/AST/Program.cs +++ b/Source/Core/AST/Program.cs @@ -400,7 +400,7 @@ public List /*!*/ GlobalVariables } } - public readonly ISet AllCoveredElements = new HashSet(); + public readonly ISet AllCoveredElements = new HashSet(); public IEnumerable Blocks() { diff --git a/Source/Core/ProgramElement.cs b/Source/Core/ProgramElement.cs new file mode 100644 index 000000000..c4aef192e --- /dev/null +++ b/Source/Core/ProgramElement.cs @@ -0,0 +1,103 @@ +using System; + +namespace Microsoft.Boogie +{ + public abstract record ProgramElement() + { + public abstract string SolverLabel { get; } + + // This suffix indicates that an ID string represents the assumption of + // a specific ensures clause after a specific call. + protected const string ensuresSuffix = "ensures"; + + // This suffix indicates that an ID string represents the goal of + // proving a specific requires clause before a specific call. + protected const string requiresSuffix = "requires"; + + // This suffix indicates that an ID string represents the assumption + // of a specific requires clause after a specific call. + protected const string requiresAssumedSuffix = "requires_assumed"; + + // This suffix indicates that an ID string represents the goal of + // proving that a specific loop invariant is established. + protected const string establishedSuffix = "established"; + + // This suffix indicates that an ID string represents the goal of + // proving that a specific loop invariant is maintained. + protected const string maintainedSuffix = "maintained"; + + // This suffix indicates that an ID string represents the asssumption + // of a specific loop invariant in the body of the loop. + protected const string assumeInBodySuffix = "assume_in_body"; + + public static ProgramElement ParseSolverString(string idString) + { + var parts = idString.Split('$'); + if (parts.Length == 3 && parts[2].Equals(requiresSuffix)) { + var reqId = parts[0]; + var callId = parts[1]; + return new CallRequiresGoalElement(callId, reqId); + } + else if (parts.Length == 3 && parts[2].Equals(requiresAssumedSuffix)) { + var reqId = parts[0]; + var callId = parts[1]; + return new CallRequiresAssumedElement(callId, reqId); + } + else if (parts.Length == 3 && parts[2].Equals(ensuresSuffix)) { + var ensId = parts[0]; + var callId = parts[1]; + return new CallEnsuresElement(callId, ensId); + } + else if (parts.Length == 2 && parts[1].Equals(establishedSuffix)) { + return new InvariantEstablishedElement(parts[0]); + } + else if (parts.Length == 2 && parts[1].Equals(maintainedSuffix)) { + return new InvariantMaintainedElement(parts[0]); + } + else if (parts.Length == 2 && parts[1].Equals(assumeInBodySuffix)) { + return new InvariantAssumedElement(parts[0]); + } + else if (parts.Length > 1) { + throw new ArgumentException($"Malformed program element ID string: {idString}"); + } + else { + return new LabeledElement(idString); + } + } + } + + public record LabeledElement(string id) : ProgramElement() + { + public override string SolverLabel => id; + } + + public record CallRequiresGoalElement(string callId, string requiresId) : ProgramElement() + { + public override string SolverLabel => $"{requiresId}${callId}${requiresSuffix}"; + } + + public record CallRequiresAssumedElement(string callId, string requiresId) : ProgramElement() + { + public override string SolverLabel => $"{requiresId}${callId}${requiresAssumedSuffix}"; + } + + public record CallEnsuresElement(string callId, string ensuresId) : ProgramElement() + { + public override string SolverLabel => $"{ensuresId}${callId}${ensuresSuffix}"; + } + + public record InvariantAssumedElement(string invariantId) : ProgramElement() + { + public override string SolverLabel => $"{invariantId}${assumeInBodySuffix}"; + } + + public record InvariantEstablishedElement(string invariantId) : ProgramElement() + { + public override string SolverLabel => $"{invariantId}${establishedSuffix}"; + } + + public record InvariantMaintainedElement(string invariantId) : ProgramElement() + { + public override string SolverLabel => $"{invariantId}${maintainedSuffix}"; + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 1eec9f43c..16c338ffe 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -674,7 +674,13 @@ private async Task VerifyEachImplementation(TextWriter output, } if (Options.Trace && Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { - Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s))); + Options.OutputWriter.WriteLine("Elements covered by verification: {0}", + string.Join(", ", + processedProgram + .Program + .AllCoveredElements + .Select(elt => elt.SolverLabel) + .OrderBy(s => s))); } cce.NonNull(Options.TheProverFactory).Close(); diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index b569e55d2..8ac34d983 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -126,7 +126,7 @@ public class HoudiniStatistics private readonly Houdini houdini; public HoudiniStatistics stats; public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public HashSet CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; ConditionGeneration.VerificationResultCollector collector; diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index fa6ba0c2b..adce6173e 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -112,7 +112,7 @@ protected ErrorHandler(SMTLibOptions options) this.options = options; } - public virtual void AddCoveredElement(string id) + public virtual void AddCoveredElement(ProgramElement elt) { throw new System.NotImplementedException(); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 1f5693470..2bbb8f46c 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -223,9 +223,8 @@ public async Task CheckSat(CancellationToken cancellationToken, if (resp.Name != "") { usedNamedAssumes.Add(resp.Name); - if (libOptions.TrackVerificationCoverage) - { - reporter.AddCoveredElement(resp.Name.Substring("aux$$assume$$".Length)); + if (libOptions.TrackVerificationCoverage) { + reporter.AddCoveredElement(new LabeledElement(resp.Name.Substring("aux$$assume$$".Length))); } } @@ -234,7 +233,7 @@ public async Task CheckSat(CancellationToken cancellationToken, usedNamedAssumes.Add(arg.Name); if (libOptions.TrackVerificationCoverage) { - reporter.AddCoveredElement(arg.Name.Substring("aux$$assume$$".Length)); + reporter.AddCoveredElement(new LabeledElement(arg.Name.Substring("aux$$assume$$".Length))); } } } diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index 752fb4372..0f019f970 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -8,5 +8,5 @@ public interface ProofRun { List Counterexamples { get; } - HashSet CoveredElements { get; } + HashSet CoveredElements { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index baca4e26d..e91eb7ed6 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1281,7 +1281,7 @@ public int GetHashCode(List obj) } if (options.Trace && options.TrackVerificationCoverage) { run.OutputWriter.WriteLine("Covered elements: {0}", - string.Join(", ", CoveredElements.OrderBy(s => s))); + string.Join(", ", CoveredElements.Select(s => s.SolverLabel).OrderBy(s => s))); } var resourceCount = await checker.GetProverResourceCount(); @@ -1309,7 +1309,7 @@ public int GetHashCode(List obj) public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public HashSet CoveredElements { get; } = new(); /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 8d9c5066d..8ec95b968 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -462,10 +462,10 @@ void ObjectInvariant() Program program; - public override void AddCoveredElement(string id) + public override void AddCoveredElement(ProgramElement elt) { - program.AllCoveredElements.Add(id); - split.CoveredElements.Add(id); + program.AllCoveredElements.Add(elt); + split.CoveredElements.Add(elt); } public ErrorReporter(VCGenOptions options, @@ -732,7 +732,8 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary new InvariantEstablishedElement(id)); prefixOfPredicateCmdsInit.Add(initAssertCmd); @@ -757,13 +758,15 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary new InvariantMaintainedElement(id)); prefixOfPredicateCmdsMaintained.Add(maintainedAssertCmd); AssumeCmd assume = new AssumeCmd(assertCmd.tok, assertCmd.Expr); // Copy any {:id ...} from the invariant to the assumption used within the body, so // we can track it while analyzing verification coverage. - (assume as ICarriesAttributes).CopyIdWithSuffixFrom(assertCmd.tok, assertCmd, "$assume_in_body"); + (assume as ICarriesAttributes).CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, + id => new InvariantAssumedElement(id)); header.Cmds[i] = assume; } diff --git a/Source/VCGeneration/VCResult.cs b/Source/VCGeneration/VCResult.cs index a3b8956f5..5613d87bc 100644 --- a/Source/VCGeneration/VCResult.cs +++ b/Source/VCGeneration/VCResult.cs @@ -25,7 +25,7 @@ public record VCResult int maxCounterExamples, List counterExamples, List asserts, - IEnumerable coveredElements, + IEnumerable coveredElements, int resourceCount, SolverKind? solverUsed ) { From f52e6c10226659b72466d9adabb716b4b27ecf06 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 1 Sep 2023 16:48:18 -0700 Subject: [PATCH 03/10] Remove unintended change --- Source/Provers/SMTLib/SMTLibProcess.cs | 9 --------- 1 file changed, 9 deletions(-) diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index b04e6a527..5a6211f45 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -58,7 +58,6 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options) { solver = new Process(); solver.StartInfo = psi; - solver.EnableRaisingEvents = true; solver.ErrorDataReceived += SolverErrorDataReceived; solver.OutputDataReceived += SolverOutputDataReceived; solver.Exited += SolverExited; @@ -75,14 +74,6 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options) private void SolverExited(object sender, EventArgs e) { - if (options.Verbosity >= 2) { - Console.WriteLine($"[SMT-ERR-{{0}}] Solver exited with code {solver.ExitCode}."); - } - - if (solver.ExitCode != 0) { - HandleError($"Solver exited with code {solver.ExitCode}"); - } - lock (this) { while (outputReceivers.TryDequeue(out var source)) { source.SetResult(null); From af6c231f0afb2e004dd0428c61c9c4b132d8b92e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 09:16:10 -0700 Subject: [PATCH 04/10] Rename ProgramElement -> TrackedNodeComponent --- Source/Core/AST/Absy.cs | 2 +- Source/Core/AST/AbsyCmd.cs | 6 ++-- Source/Core/AST/Program.cs | 2 +- ...gramElement.cs => TrackedNodeComponent.cs} | 32 +++++++++---------- Source/Houdini/HoudiniSession.cs | 2 +- Source/Provers/SMTLib/ProverInterface.cs | 2 +- .../SMTLib/SMTLibInteractiveTheoremProver.cs | 4 +-- Source/VCGeneration/ProofRun.cs | 2 +- Source/VCGeneration/Split.cs | 2 +- Source/VCGeneration/VCGen.cs | 8 ++--- Source/VCGeneration/VCResult.cs | 2 +- 11 files changed, 32 insertions(+), 32 deletions(-) rename Source/Core/{ProgramElement.cs => TrackedNodeComponent.cs} (70%) diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 28c7ffd51..21c627291 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -300,7 +300,7 @@ public void CopyIdFrom(IToken tok, ICarriesAttributes src) } } - public void CopyIdWithModificationsFrom(IToken tok, ICarriesAttributes src, Func modifier) + public void CopyIdWithModificationsFrom(IToken tok, ICarriesAttributes src, Func modifier) { var id = src.FindStringAttribute("id"); if (id is not null) { diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 990c18721..e0bda007c 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -3853,7 +3853,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) // Do this after copying the attributes so it doesn't get overwritten if (callId is not null) { (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, - id => new CallRequiresGoalElement(callId, id)); + id => new TrackedCallRequiresGoal(callId, id)); } a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; @@ -3870,7 +3870,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) // These probably won't have IDs, but copy if they do. if (callId is not null) { (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, - id => new CallRequiresAssumedElement(callId, id)); + id => new TrackedCallRequiresAssumed(callId, id)); } newBlockBody.Add(a); @@ -4037,7 +4037,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) if (callId is not null) { (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e, - id => new CallEnsuresElement(callId, id)); + id => new TrackedCallEnsures(callId, id)); } newBlockBody.Add(assume); diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index 50d7dabb2..b69feca1b 100644 --- a/Source/Core/AST/Program.cs +++ b/Source/Core/AST/Program.cs @@ -400,7 +400,7 @@ public List /*!*/ GlobalVariables } } - public readonly ISet AllCoveredElements = new HashSet(); + public readonly ISet AllCoveredElements = new HashSet(); public IEnumerable Blocks() { diff --git a/Source/Core/ProgramElement.cs b/Source/Core/TrackedNodeComponent.cs similarity index 70% rename from Source/Core/ProgramElement.cs rename to Source/Core/TrackedNodeComponent.cs index c4aef192e..8d36a8f95 100644 --- a/Source/Core/ProgramElement.cs +++ b/Source/Core/TrackedNodeComponent.cs @@ -2,7 +2,7 @@ namespace Microsoft.Boogie { - public abstract record ProgramElement() + public abstract record TrackedNodeComponent() { public abstract string SolverLabel { get; } @@ -30,73 +30,73 @@ public abstract record ProgramElement() // of a specific loop invariant in the body of the loop. protected const string assumeInBodySuffix = "assume_in_body"; - public static ProgramElement ParseSolverString(string idString) + public static TrackedNodeComponent ParseSolverString(string idString) { var parts = idString.Split('$'); if (parts.Length == 3 && parts[2].Equals(requiresSuffix)) { var reqId = parts[0]; var callId = parts[1]; - return new CallRequiresGoalElement(callId, reqId); + return new TrackedCallRequiresGoal(callId, reqId); } else if (parts.Length == 3 && parts[2].Equals(requiresAssumedSuffix)) { var reqId = parts[0]; var callId = parts[1]; - return new CallRequiresAssumedElement(callId, reqId); + return new TrackedCallRequiresAssumed(callId, reqId); } else if (parts.Length == 3 && parts[2].Equals(ensuresSuffix)) { var ensId = parts[0]; var callId = parts[1]; - return new CallEnsuresElement(callId, ensId); + return new TrackedCallEnsures(callId, ensId); } else if (parts.Length == 2 && parts[1].Equals(establishedSuffix)) { - return new InvariantEstablishedElement(parts[0]); + return new TrackedInvariantEstablished(parts[0]); } else if (parts.Length == 2 && parts[1].Equals(maintainedSuffix)) { - return new InvariantMaintainedElement(parts[0]); + return new TrackedInvariantMaintained(parts[0]); } else if (parts.Length == 2 && parts[1].Equals(assumeInBodySuffix)) { - return new InvariantAssumedElement(parts[0]); + return new TrackedInvariantAssumed(parts[0]); } else if (parts.Length > 1) { throw new ArgumentException($"Malformed program element ID string: {idString}"); } else { - return new LabeledElement(idString); + return new LabeledNodeComponent(idString); } } } - public record LabeledElement(string id) : ProgramElement() + public record LabeledNodeComponent(string id) : TrackedNodeComponent() { public override string SolverLabel => id; } - public record CallRequiresGoalElement(string callId, string requiresId) : ProgramElement() + public record TrackedCallRequiresGoal(string callId, string requiresId) : TrackedNodeComponent() { public override string SolverLabel => $"{requiresId}${callId}${requiresSuffix}"; } - public record CallRequiresAssumedElement(string callId, string requiresId) : ProgramElement() + public record TrackedCallRequiresAssumed(string callId, string requiresId) : TrackedNodeComponent() { public override string SolverLabel => $"{requiresId}${callId}${requiresAssumedSuffix}"; } - public record CallEnsuresElement(string callId, string ensuresId) : ProgramElement() + public record TrackedCallEnsures(string callId, string ensuresId) : TrackedNodeComponent() { public override string SolverLabel => $"{ensuresId}${callId}${ensuresSuffix}"; } - public record InvariantAssumedElement(string invariantId) : ProgramElement() + public record TrackedInvariantAssumed(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${assumeInBodySuffix}"; } - public record InvariantEstablishedElement(string invariantId) : ProgramElement() + public record TrackedInvariantEstablished(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${establishedSuffix}"; } - public record InvariantMaintainedElement(string invariantId) : ProgramElement() + public record TrackedInvariantMaintained(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${maintainedSuffix}"; } diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 8ac34d983..587443612 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -126,7 +126,7 @@ public class HoudiniStatistics private readonly Houdini houdini; public HoudiniStatistics stats; public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public HashSet CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; ConditionGeneration.VerificationResultCollector collector; diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index adce6173e..2ed73ad73 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -112,7 +112,7 @@ protected ErrorHandler(SMTLibOptions options) this.options = options; } - public virtual void AddCoveredElement(ProgramElement elt) + public virtual void AddCoveredElement(TrackedNodeComponent elt) { throw new System.NotImplementedException(); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 2bbb8f46c..8a8aef2b7 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -224,7 +224,7 @@ public async Task CheckSat(CancellationToken cancellationToken, { usedNamedAssumes.Add(resp.Name); if (libOptions.TrackVerificationCoverage) { - reporter.AddCoveredElement(new LabeledElement(resp.Name.Substring("aux$$assume$$".Length))); + reporter.AddCoveredElement(new LabeledNodeComponent(resp.Name.Substring("aux$$assume$$".Length))); } } @@ -233,7 +233,7 @@ public async Task CheckSat(CancellationToken cancellationToken, usedNamedAssumes.Add(arg.Name); if (libOptions.TrackVerificationCoverage) { - reporter.AddCoveredElement(new LabeledElement(arg.Name.Substring("aux$$assume$$".Length))); + reporter.AddCoveredElement(new LabeledNodeComponent(arg.Name.Substring("aux$$assume$$".Length))); } } } diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index 0f019f970..f1f38e9af 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -8,5 +8,5 @@ public interface ProofRun { List Counterexamples { get; } - HashSet CoveredElements { get; } + HashSet CoveredElements { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index e91eb7ed6..0e73b8e01 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1309,7 +1309,7 @@ public int GetHashCode(List obj) public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public HashSet CoveredElements { get; } = new(); /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 8ec95b968..b9296a805 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -462,7 +462,7 @@ void ObjectInvariant() Program program; - public override void AddCoveredElement(ProgramElement elt) + public override void AddCoveredElement(TrackedNodeComponent elt) { program.AllCoveredElements.Add(elt); split.CoveredElements.Add(elt); @@ -733,7 +733,7 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary new InvariantEstablishedElement(id)); + id => new TrackedInvariantEstablished(id)); prefixOfPredicateCmdsInit.Add(initAssertCmd); @@ -759,14 +759,14 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary new InvariantMaintainedElement(id)); + id => new TrackedInvariantMaintained(id)); prefixOfPredicateCmdsMaintained.Add(maintainedAssertCmd); AssumeCmd assume = new AssumeCmd(assertCmd.tok, assertCmd.Expr); // Copy any {:id ...} from the invariant to the assumption used within the body, so // we can track it while analyzing verification coverage. (assume as ICarriesAttributes).CopyIdWithModificationsFrom(assertCmd.tok, assertCmd, - id => new InvariantAssumedElement(id)); + id => new TrackedInvariantAssumed(id)); header.Cmds[i] = assume; } diff --git a/Source/VCGeneration/VCResult.cs b/Source/VCGeneration/VCResult.cs index 5613d87bc..a304b1158 100644 --- a/Source/VCGeneration/VCResult.cs +++ b/Source/VCGeneration/VCResult.cs @@ -25,7 +25,7 @@ public record VCResult int maxCounterExamples, List counterExamples, List asserts, - IEnumerable coveredElements, + IEnumerable coveredElements, int resourceCount, SolverKind? solverUsed ) { From e0c1c7d7f108949e1c28d706e5a020ec36a1ed86 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 09:16:17 -0700 Subject: [PATCH 05/10] Bump version --- Source/Directory.Build.props | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index 7c18b996c..6e42ab740 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.0.1 + 3.0.2 net6.0 false Boogie From cc679901ebaca1ff863b69632cc9fe9503f16723 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 09:23:02 -0700 Subject: [PATCH 06/10] Added comment --- Source/Core/TrackedNodeComponent.cs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Source/Core/TrackedNodeComponent.cs b/Source/Core/TrackedNodeComponent.cs index 8d36a8f95..fac55433f 100644 --- a/Source/Core/TrackedNodeComponent.cs +++ b/Source/Core/TrackedNodeComponent.cs @@ -2,6 +2,9 @@ namespace Microsoft.Boogie { + // Represents an AST node, or component of a node, that is being + // tracked during the proof process to determine whether it was + // used as part of a completed proof. public abstract record TrackedNodeComponent() { public abstract string SolverLabel { get; } From 3b8ee1499f5ec375a204f13fb192c3919823b4f6 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 14:55:25 -0700 Subject: [PATCH 07/10] Actually parse UNSAT core labels from solver --- Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 8a8aef2b7..a23a437f9 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -224,7 +224,7 @@ public async Task CheckSat(CancellationToken cancellationToken, { usedNamedAssumes.Add(resp.Name); if (libOptions.TrackVerificationCoverage) { - reporter.AddCoveredElement(new LabeledNodeComponent(resp.Name.Substring("aux$$assume$$".Length))); + reporter.AddCoveredElement(TrackedNodeComponent.ParseSolverString(resp.Name.Substring("aux$$assume$$".Length))); } } @@ -233,7 +233,7 @@ public async Task CheckSat(CancellationToken cancellationToken, usedNamedAssumes.Add(arg.Name); if (libOptions.TrackVerificationCoverage) { - reporter.AddCoveredElement(new LabeledNodeComponent(arg.Name.Substring("aux$$assume$$".Length))); + reporter.AddCoveredElement(TrackedNodeComponent.ParseSolverString(arg.Name.Substring("aux$$assume$$".Length))); } } } From 7a87d2d0bf0fdfbe54523c8b971bfe36fbe66517 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 15:17:03 -0700 Subject: [PATCH 08/10] Test that tracked nodes are parsed --- Source/Core/TrackedNodeComponent.cs | 9 ++ Source/ExecutionEngine/ExecutionEngine.cs | 6 +- Source/VCGeneration/Split.cs | 4 +- Test/coverage/verificationCoverage.bpl | 104 +++++++++++++++++++--- 4 files changed, 104 insertions(+), 19 deletions(-) diff --git a/Source/Core/TrackedNodeComponent.cs b/Source/Core/TrackedNodeComponent.cs index fac55433f..7749f3722 100644 --- a/Source/Core/TrackedNodeComponent.cs +++ b/Source/Core/TrackedNodeComponent.cs @@ -9,6 +9,8 @@ public abstract record TrackedNodeComponent() { public abstract string SolverLabel { get; } + public abstract string Description { get; } + // This suffix indicates that an ID string represents the assumption of // a specific ensures clause after a specific call. protected const string ensuresSuffix = "ensures"; @@ -72,35 +74,42 @@ public static TrackedNodeComponent ParseSolverString(string idString) public record LabeledNodeComponent(string id) : TrackedNodeComponent() { public override string SolverLabel => id; + public override string Description => id; } public record TrackedCallRequiresGoal(string callId, string requiresId) : TrackedNodeComponent() { public override string SolverLabel => $"{requiresId}${callId}${requiresSuffix}"; + public override string Description => $"requires clause {requiresId} proved for call {callId}"; } public record TrackedCallRequiresAssumed(string callId, string requiresId) : TrackedNodeComponent() { public override string SolverLabel => $"{requiresId}${callId}${requiresAssumedSuffix}"; + public override string Description => $"requires clause {requiresId} assumed from call {callId}"; } public record TrackedCallEnsures(string callId, string ensuresId) : TrackedNodeComponent() { public override string SolverLabel => $"{ensuresId}${callId}${ensuresSuffix}"; + public override string Description => $"ensures clause {ensuresId} from call {callId}"; } public record TrackedInvariantAssumed(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${assumeInBodySuffix}"; + public override string Description => $"invariant {invariantId} assumed in body"; } public record TrackedInvariantEstablished(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${establishedSuffix}"; + public override string Description => $"invariant {invariantId} established"; } public record TrackedInvariantMaintained(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${maintainedSuffix}"; + public override string Description => $"invariant {invariantId} maintained"; } } \ No newline at end of file diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 16c338ffe..9b7c3e925 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -674,12 +674,12 @@ private async Task VerifyEachImplementation(TextWriter output, } if (Options.Trace && Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { - Options.OutputWriter.WriteLine("Elements covered by verification: {0}", - string.Join(", ", + Options.OutputWriter.WriteLine("Proof dependencies of whole program:\n {0}", + string.Join("\n ", processedProgram .Program .AllCoveredElements - .Select(elt => elt.SolverLabel) + .Select(elt => elt.Description) .OrderBy(s => s))); } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 0e73b8e01..9b847c7ac 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1280,8 +1280,8 @@ public int GetHashCode(List obj) checker.ProverRunTime.TotalSeconds, outcome); } if (options.Trace && options.TrackVerificationCoverage) { - run.OutputWriter.WriteLine("Covered elements: {0}", - string.Join(", ", CoveredElements.Select(s => s.SolverLabel).OrderBy(s => s))); + run.OutputWriter.WriteLine("Proof dependencies:\n {0}", + string.Join("\n ", CoveredElements.Select(s => s.Description).OrderBy(s => s))); } var resourceCount = await checker.GetProverResourceCount(); diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index d2a38020a..e19d1aace 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -1,18 +1,94 @@ // RUN: %boogie "%s" > "%t.plain" // RUN: %diff "%s.expect" "%t.plain" // RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t.coverage" -// RUN %OutputCheck "%s" --file-to-check="%t.coverage" -// CHECK: Covered elements: a0, assert_a0, assert_r0, r0 -// CHECK: Covered elements: sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1 -// CHECK: Covered elements: cont_assume_1, cont_assume_2 -// CHECK: Covered elements: false_req -// CHECK: Covered elements: cont_req_1, cont_req_2 -// CHECK: Covered elements: assumeFalse -// CHECK: Covered elements: tee0, tee1, ter0 -// CHECK: Covered elements: call2_tee1, tee_not_1, tee0$call1$ensures, tee0$call2$ensures, tee1$call2$ensures, ter0$call1$requires, ter0$call2$requires, ter1, xy_sum -// CHECK: Covered elements: a_gt_10, constrained, x_gt_10 -// CHECK: Covered elements: cont_ens_abs$call_cont$ensures, xpos_abs$call_cont$requires, xpos_caller -// CHECK: Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, call2_tee1, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, tee1$call2$ensures, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum +// RUN: %OutputCheck "%s" --file-to-check="%t.coverage" +// CHECK: Proof dependencies: +// CHECK: a0 +// CHECK: assert_a0 +// CHECK: assert_r0 +// CHECK: r0 +// CHECK: Proof dependencies: +// CHECK: invariant sinv_not_1 established +// CHECK: invariant sinv_not_1 maintained +// CHECK: invariant sinv1 assumed in body +// CHECK: invariant sinv1 established +// CHECK: invariant sinv1 maintained +// CHECK: invariant sinv2 assumed in body +// CHECK: invariant sinv2 established +// CHECK: invariant sinv2 maintained +// CHECK: spost +// CHECK: spre1 +// CHECK: Proof dependencies: +// CHECK: cont_assume_1 +// CHECK: cont_assume_2 +// CHECK: Proof dependencies: +// CHECK: false_req +// CHECK: Proof dependencies: +// CHECK: cont_req_1 +// CHECK: cont_req_2 +// CHECK: Proof dependencies: +// CHECK: assumeFalse +// CHECK: Proof dependencies: +// CHECK: tee0 +// CHECK: tee1 +// CHECK: ter0 +// CHECK: Proof dependencies: +// CHECK: call2_tee1 +// CHECK: ensures clause tee0 from call call1 +// CHECK: ensures clause tee0 from call call2 +// CHECK: ensures clause tee1 from call call2 +// CHECK: requires clause ter0 proved for call call1 +// CHECK: requires clause ter0 proved for call call2 +// CHECK: tee_not_1 +// CHECK: ter1 +// CHECK: xy_sum +// CHECK: Proof dependencies: +// CHECK: a_gt_10 +// CHECK: constrained +// CHECK: x_gt_10 +// CHECK: Proof dependencies: +// CHECK: ensures clause cont_ens_abs from call call_cont +// CHECK: requires clause xpos_abs proved for call call_cont +// CHECK: xpos_caller +// CHECK: Proof dependencies of whole program: +// CHECK: a_gt_10 +// CHECK: a0 +// CHECK: assert_a0 +// CHECK: assert_r0 +// CHECK: assumeFalse +// CHECK: call2_tee1 +// CHECK: constrained +// CHECK: cont_assume_1 +// CHECK: cont_assume_2 +// CHECK: cont_req_1 +// CHECK: cont_req_2 +// CHECK: ensures clause cont_ens_abs from call call_cont +// CHECK: ensures clause tee0 from call call1 +// CHECK: ensures clause tee0 from call call2 +// CHECK: ensures clause tee1 from call call2 +// CHECK: false_req +// CHECK: invariant sinv_not_1 established +// CHECK: invariant sinv_not_1 maintained +// CHECK: invariant sinv1 assumed in body +// CHECK: invariant sinv1 established +// CHECK: invariant sinv1 maintained +// CHECK: invariant sinv2 assumed in body +// CHECK: invariant sinv2 established +// CHECK: invariant sinv2 maintained +// CHECK: r0 +// CHECK: requires clause ter0 proved for call call1 +// CHECK: requires clause ter0 proved for call call2 +// CHECK: requires clause xpos_abs proved for call call_cont +// CHECK: spost +// CHECK: spre1 +// CHECK: tee_not_1 +// CHECK: tee0 +// CHECK: tee1 +// CHECK: ter0 +// CHECK: ter1 +// CHECK: x_gt_10 +// CHECK: xpos_caller +// CHECK: xy_sum // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage" // RUN: %diff "%s.expect" "%t.coverage" // RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune "%s" > "%t.coverage-a" @@ -21,8 +97,8 @@ // RUN: %diff "%s.expect" "%t.coverage-p" // RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune "%s" > "%t.coverage-d" // RUN: %diff "%s.expect" "%t.coverage-d" -// RUN %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n" -// RUN %diff "%s.expect" "%t.coverage-n" +// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n" +// RUN: %diff "%s.expect" "%t.coverage-n" // UNSUPPORTED: batch_mode procedure testRequiresAssign(n: int) From 5555600c79e7f02e4dcb2bb4105f0cfcf3ed6f88 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 15:29:11 -0700 Subject: [PATCH 09/10] Update some comments --- Source/Core/TrackedNodeComponent.cs | 55 +++++++++++++++++++++-------- 1 file changed, 40 insertions(+), 15 deletions(-) diff --git a/Source/Core/TrackedNodeComponent.cs b/Source/Core/TrackedNodeComponent.cs index 7749f3722..2f25f518e 100644 --- a/Source/Core/TrackedNodeComponent.cs +++ b/Source/Core/TrackedNodeComponent.cs @@ -2,39 +2,64 @@ namespace Microsoft.Boogie { - // Represents an AST node, or component of a node, that is being - // tracked during the proof process to determine whether it was - // used as part of a completed proof. + /// + /// Represents an AST node, or component of a node, that is being + /// tracked during the proof process to determine whether it was + /// used as part of a completed proof. + /// public abstract record TrackedNodeComponent() { + /// + /// The string used to represent this component in the solver. + /// public abstract string SolverLabel { get; } + /// + /// A human-readable description of this component in terms of + /// user-provided :id attributes. + /// public abstract string Description { get; } - // This suffix indicates that an ID string represents the assumption of - // a specific ensures clause after a specific call. + /// + /// This suffix indicates that an ID string represents the assumption of + /// a specific ensures clause after a specific call. + /// protected const string ensuresSuffix = "ensures"; - // This suffix indicates that an ID string represents the goal of - // proving a specific requires clause before a specific call. + /// + /// This suffix indicates that an ID string represents the goal of + /// proving a specific requires clause before a specific call. + /// protected const string requiresSuffix = "requires"; - // This suffix indicates that an ID string represents the assumption - // of a specific requires clause after a specific call. + /// + /// This suffix indicates that an ID string represents the assumption + /// of a specific requires clause after a specific call. + /// protected const string requiresAssumedSuffix = "requires_assumed"; - // This suffix indicates that an ID string represents the goal of - // proving that a specific loop invariant is established. + /// + /// This suffix indicates that an ID string represents the goal of + /// proving that a specific loop invariant is established. + /// protected const string establishedSuffix = "established"; - // This suffix indicates that an ID string represents the goal of - // proving that a specific loop invariant is maintained. + /// + /// This suffix indicates that an ID string represents the goal of + /// proving that a specific loop invariant is maintained. + /// protected const string maintainedSuffix = "maintained"; - // This suffix indicates that an ID string represents the asssumption - // of a specific loop invariant in the body of the loop. + /// + /// This suffix indicates that an ID string represents the asssumption + /// of a specific loop invariant in the body of the loop. + /// protected const string assumeInBodySuffix = "assume_in_body"; + /// + /// Reverse the transformation of TrackedNodeComponent to string + /// done by the SolverLabel attribute. + /// public static TrackedNodeComponent ParseSolverString(string idString) { var parts = idString.Split('$'); From d0a04e7eebe330406d808a89d20558d7d4c1685d Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 15:43:46 -0700 Subject: [PATCH 10/10] Fix expected output of other test --- Test/unnecessaryassumes/unnecessaryassumes1.bpl | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl index e5ec0bbbe..70c9a2bd3 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -1,9 +1,15 @@ // We use boogie instead of parallel-boogie here to fix the order of the output from /trackVerificationCoverage // RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t" -// CHECK: Covered elements: s0 -// CHECK: Covered elements: s2, s3 -// CHECK: Elements covered by verification: s0, s2, s3 +// CHECK: Proof dependencies: +// CHECK: s0 +// CHECK: Proof dependencies: +// CHECK: s2 +// CHECK: s3 +// CHECK: Proof dependencies of whole program: +// CHECK: s0 +// CHECK: s2 +// CHECK: s3 // UNSUPPORTED: batch_mode procedure test0(n: int)