diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs index b47bfae5f..16649a7ab 100644 --- a/Source/ExecutionEngine/ConsolePrinter.cs +++ b/Source/ExecutionEngine/ConsolePrinter.cs @@ -206,11 +206,11 @@ public virtual void ReportStartVerifyImplementation(Implementation implementatio // Do not print anything to console } - public virtual void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) { + public virtual void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) { // Do not print anything to console } - public virtual void ReportSplitResult(Split split, VCResult splitResult) { + public virtual void ReportSplitResult(Split split, VerificationRunResult splitResult) { // Do not print anything to console } } diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index ed96e80f4..467cca178 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -19,7 +19,7 @@ namespace Microsoft.Boogie { - public record ProcessedProgram(Program Program, Action PostProcessResult) { + public record ProcessedProgram(Program Program, Action PostProcessResult) { public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) { } } @@ -828,10 +828,10 @@ private IObservable VerifyImplementation( string programId, TextWriter traceWriter) { - VerificationResult verificationResult = GetCachedVerificationResult(implementation, traceWriter); - if (verificationResult != null) { - UpdateCachedStatistics(stats, verificationResult.Outcome, verificationResult.Errors); - return Observable.Return(new Completed(verificationResult)); + ImplementationRunResult implementationRunResult = GetCachedVerificationResult(implementation, traceWriter); + if (implementationRunResult != null) { + UpdateCachedStatistics(stats, implementationRunResult.VcOutcome, implementationRunResult.Errors); + return Observable.Return(new Completed(implementationRunResult)); } Options.Printer.Inform("", traceWriter); // newline Options.Printer.Inform($"Verifying {implementation.VerboseName} ...", traceWriter); @@ -849,7 +849,7 @@ private IObservable VerifyImplementation( return Observable.Return(new Running()).Concat(afterRunningStates); } - public VerificationResult GetCachedVerificationResult(Implementation impl, TextWriter output) + public ImplementationRunResult GetCachedVerificationResult(Implementation impl, TextWriter output) { if (0 >= Options.VerifySnapshots) { @@ -863,7 +863,7 @@ public VerificationResult GetCachedVerificationResult(Implementation impl, TextW } if (Options.VerifySnapshots < 3 || - cachedResults.Outcome == ConditionGeneration.Outcome.Correct) { + cachedResults.VcOutcome == VcOutcome.Correct) { Options.Printer.Inform($"Retrieving cached verification result for implementation {impl.VerboseName}...", output); return cachedResults; } @@ -875,9 +875,9 @@ private IObservable VerifyImplementationWithoutCaching(Proc PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken, string programId, Implementation impl, TextWriter traceWriter) { - var verificationResult = new VerificationResult(impl, programId); + var verificationResult = new ImplementationRunResult(impl, programId); - var batchCompleted = new Subject<(Split split, VCResult vcResult)>(); + var batchCompleted = new Subject<(Split split, VerificationRunResult vcResult)>(); var completeVerification = largeThreadTaskFactory.StartNew(async () => { var vcgen = new VCGen(processedProgram.Program, checkerPool); @@ -887,7 +887,7 @@ private IObservable VerifyImplementationWithoutCaching(Proc try { - (verificationResult.Outcome, verificationResult.Errors, verificationResult.VCResults) = + (verificationResult.VcOutcome, verificationResult.Errors, verificationResult.VCResults) = await vcgen.VerifyImplementation(new ImplementationRun(impl, traceWriter), batchCompleted, cancellationToken); processedProgram.PostProcessResult(vcgen, impl, verificationResult); } @@ -906,7 +906,7 @@ private IObservable VerifyImplementationWithoutCaching(Proc } verificationResult.Errors = null; - verificationResult.Outcome = ConditionGeneration.Outcome.Inconclusive; + verificationResult.VcOutcome = VcOutcome.Inconclusive; } catch (ProverDiedException) { @@ -918,14 +918,14 @@ private IObservable VerifyImplementationWithoutCaching(Proc "Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.VerboseName, upo.Message); verificationResult.Errors = null; - verificationResult.Outcome = ConditionGeneration.Outcome.Inconclusive; + verificationResult.VcOutcome = VcOutcome.Inconclusive; } catch (IOException e) { Options.Printer.AdvisoryWriteLine(traceWriter, "Advisory: {0} SKIPPED due to I/O exception: {1}", impl.VerboseName, e.Message); verificationResult.Errors = null; - verificationResult.Outcome = ConditionGeneration.Outcome.SolverException; + verificationResult.VcOutcome = VcOutcome.SolverException; } verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount; @@ -993,8 +993,8 @@ private async Task RunHoudini(Program program, PipelineStatisti foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) { - ProcessOutcome(Options.Printer, x.outcome, x.errors, "", stats, outputWriter, Options.TimeLimit, er); - ProcessErrors(Options.Printer, x.errors, x.outcome, outputWriter, er); + ProcessOutcome(Options.Printer, x.VcOutcome, x.errors, "", stats, outputWriter, Options.TimeLimit, er); + ProcessErrors(Options.Printer, x.errors, x.VcOutcome, outputWriter, er); } return PipelineOutcome.Done; @@ -1046,8 +1046,8 @@ private async Task RunStagedHoudini(Program program, PipelineSt foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) { - ProcessOutcome(Options.Printer, x.outcome, x.errors, "", stats, Options.OutputWriter, Options.TimeLimit, er); - ProcessErrors(Options.Printer, x.errors, x.outcome, Options.OutputWriter, er); + ProcessOutcome(Options.Printer, x.VcOutcome, x.errors, "", stats, Options.OutputWriter, Options.TimeLimit, er); + ProcessErrors(Options.Printer, x.errors, x.VcOutcome, Options.OutputWriter, er); } return PipelineOutcome.Done; @@ -1055,24 +1055,24 @@ private async Task RunStagedHoudini(Program program, PipelineSt #endregion - public void ProcessOutcome(OutputPrinter printer, ConditionGeneration.Outcome outcome, List errors, string timeIndication, + public void ProcessOutcome(OutputPrinter printer, VcOutcome vcOutcome, List errors, string timeIndication, PipelineStatistics stats, TextWriter tw, uint timeLimit, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string msgIfVerifies = null) { Contract.Requires(stats != null); - UpdateStatistics(stats, outcome, errors); + UpdateStatistics(stats, vcOutcome, errors); - printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw); + printer.Inform(timeIndication + OutcomeIndication(vcOutcome, errors), tw); - ReportOutcome(printer, outcome, er, implName, implTok, msgIfVerifies, tw, timeLimit, errors); + ReportOutcome(printer, vcOutcome, er, implName, implTok, msgIfVerifies, tw, timeLimit, errors); } public void ReportOutcome(OutputPrinter printer, - ConditionGeneration.Outcome outcome, ErrorReporterDelegate er, string implName, + VcOutcome vcOutcome, ErrorReporterDelegate er, string implName, IToken implTok, string msgIfVerifies, TextWriter tw, uint timeLimit, List errors) { - var errorInfo = GetOutcomeError(Options, outcome, implName, implTok, msgIfVerifies, tw, timeLimit, errors); + var errorInfo = GetOutcomeError(Options, vcOutcome, implName, implTok, msgIfVerifies, tw, timeLimit, errors); if (errorInfo != null) { errorInfo.ImplementationName = implName; @@ -1088,25 +1088,25 @@ public void ReportOutcome(OutputPrinter printer, } } - internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, ConditionGeneration.Outcome outcome, string implName, IToken implTok, string msgIfVerifies, + internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, VcOutcome vcOutcome, string implName, IToken implTok, string msgIfVerifies, TextWriter tw, uint timeLimit, List errors) { ErrorInformation errorInfo = null; - switch (outcome) { - case VCGen.Outcome.Correct: + switch (vcOutcome) { + case VcOutcome.Correct: if (msgIfVerifies != null) { tw.WriteLine(msgIfVerifies); } break; - case VCGen.Outcome.ReachedBound: + case VcOutcome.ReachedBound: tw.WriteLine($"Stratified Inlining: Reached recursion bound of {options.RecursionBound}"); break; - case VCGen.Outcome.Errors: - case VCGen.Outcome.TimedOut: + case VcOutcome.Errors: + case VcOutcome.TimedOut: if (implName != null && implTok != null) { - if (outcome == ConditionGeneration.Outcome.TimedOut || + if (vcOutcome == VcOutcome.TimedOut || (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) { string msg = string.Format("Verification of '{1}' timed out after {0} seconds", timeLimit, implName); errorInfo = ErrorInformation.Create(implTok, msg); @@ -1148,21 +1148,21 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, } break; - case VCGen.Outcome.OutOfResource: + case VcOutcome.OutOfResource: if (implName != null && implTok != null) { string msg = "Verification out of resource (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); } break; - case VCGen.Outcome.OutOfMemory: + case VcOutcome.OutOfMemory: if (implName != null && implTok != null) { string msg = "Verification out of memory (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); } break; - case VCGen.Outcome.SolverException: + case VcOutcome.SolverException: if (implName != null && implTok != null) { string msg = "Verification encountered solver exception (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); @@ -1170,7 +1170,7 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, break; - case VCGen.Outcome.Inconclusive: + case VcOutcome.Inconclusive: if (implName != null && implTok != null) { string msg = "Verification inconclusive (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); @@ -1183,36 +1183,36 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, } - private static string OutcomeIndication(VC.VCGen.Outcome outcome, List errors) + private static string OutcomeIndication(VcOutcome vcOutcome, List errors) { string traceOutput = ""; - switch (outcome) + switch (vcOutcome) { default: Contract.Assert(false); // unexpected outcome throw new cce.UnreachableException(); - case VCGen.Outcome.ReachedBound: + case VcOutcome.ReachedBound: traceOutput = "verified"; break; - case VCGen.Outcome.Correct: + case VcOutcome.Correct: traceOutput = "verified"; break; - case VCGen.Outcome.TimedOut: + case VcOutcome.TimedOut: traceOutput = "timed out"; break; - case VCGen.Outcome.OutOfResource: + case VcOutcome.OutOfResource: traceOutput = "out of resource"; break; - case VCGen.Outcome.OutOfMemory: + case VcOutcome.OutOfMemory: traceOutput = "out of memory"; break; - case VCGen.Outcome.SolverException: + case VcOutcome.SolverException: traceOutput = "solver exception"; break; - case VCGen.Outcome.Inconclusive: + case VcOutcome.Inconclusive: traceOutput = "inconclusive"; break; - case VCGen.Outcome.Errors: + case VcOutcome.Errors: Contract.Assert(errors != null); traceOutput = string.Format("error{0}", errors.Count == 1 ? "" : "s"); break; @@ -1222,44 +1222,44 @@ private static string OutcomeIndication(VC.VCGen.Outcome outcome, List errors) + private static void UpdateStatistics(PipelineStatistics stats, VcOutcome vcOutcome, List errors) { Contract.Requires(stats != null); - switch (outcome) + switch (vcOutcome) { default: Contract.Assert(false); // unexpected outcome throw new cce.UnreachableException(); - case VCGen.Outcome.ReachedBound: + case VcOutcome.ReachedBound: Interlocked.Increment(ref stats.VerifiedCount); break; - case VCGen.Outcome.Correct: + case VcOutcome.Correct: Interlocked.Increment(ref stats.VerifiedCount); break; - case VCGen.Outcome.TimedOut: + case VcOutcome.TimedOut: Interlocked.Increment(ref stats.TimeoutCount); break; - case VCGen.Outcome.OutOfResource: + case VcOutcome.OutOfResource: Interlocked.Increment(ref stats.OutOfResourceCount); break; - case VCGen.Outcome.OutOfMemory: + case VcOutcome.OutOfMemory: Interlocked.Increment(ref stats.OutOfMemoryCount); break; - case VCGen.Outcome.SolverException: + case VcOutcome.SolverException: Interlocked.Increment(ref stats.SolverExceptionCount); break; - case VCGen.Outcome.Inconclusive: + case VcOutcome.Inconclusive: Interlocked.Increment(ref stats.InconclusiveCount); break; - case VCGen.Outcome.Errors: + case VcOutcome.Errors: int cnt = errors.Count(e => !e.IsAuxiliaryCexForDiagnosingTimeouts); Interlocked.Add(ref stats.ErrorCount, cnt); @@ -1267,43 +1267,43 @@ private static void UpdateStatistics(PipelineStatistics stats, VC.VCGen.Outcome } } - private static void UpdateCachedStatistics(PipelineStatistics stats, VC.VCGen.Outcome outcome, List errors) { + private static void UpdateCachedStatistics(PipelineStatistics stats, VcOutcome vcOutcome, List errors) { Contract.Requires(stats != null); - switch (outcome) + switch (vcOutcome) { default: Contract.Assert(false); // unexpected outcome throw new cce.UnreachableException(); - case VCGen.Outcome.ReachedBound: + case VcOutcome.ReachedBound: Interlocked.Increment(ref stats.CachedVerifiedCount); break; - case VCGen.Outcome.Correct: + case VcOutcome.Correct: Interlocked.Increment(ref stats.CachedVerifiedCount); break; - case VCGen.Outcome.TimedOut: + case VcOutcome.TimedOut: Interlocked.Increment(ref stats.CachedTimeoutCount); break; - case VCGen.Outcome.OutOfResource: + case VcOutcome.OutOfResource: Interlocked.Increment(ref stats.CachedOutOfResourceCount); break; - case VCGen.Outcome.OutOfMemory: + case VcOutcome.OutOfMemory: Interlocked.Increment(ref stats.CachedOutOfMemoryCount); break; - case VCGen.Outcome.SolverException: + case VcOutcome.SolverException: Interlocked.Increment(ref stats.CachedSolverExceptionCount); break; - case VCGen.Outcome.Inconclusive: + case VcOutcome.Inconclusive: Interlocked.Increment(ref stats.CachedInconclusiveCount); break; - case VCGen.Outcome.Errors: + case VcOutcome.Errors: int cnt = errors.Count(e => !e.IsAuxiliaryCexForDiagnosingTimeouts); Interlocked.Add(ref stats.CachedErrorCount, cnt); @@ -1313,7 +1313,7 @@ private static void UpdateCachedStatistics(PipelineStatistics stats, VC.VCGen.Ou public void ProcessErrors(OutputPrinter printer, List errors, - ConditionGeneration.Outcome outcome, TextWriter tw, + VcOutcome vcOutcome, TextWriter tw, ErrorReporterDelegate er, Implementation impl = null) { var implName = impl?.VerboseName; @@ -1331,7 +1331,7 @@ public void ProcessErrors(OutputPrinter printer, continue; } - var errorInfo = error.CreateErrorInformation(outcome, Options.ForceBplErrors); + var errorInfo = error.CreateErrorInformation(vcOutcome, Options.ForceBplErrors); errorInfo.ImplementationName = implName; if (Options.XmlSink != null) diff --git a/Source/ExecutionEngine/VerificationResult.cs b/Source/ExecutionEngine/ImplementationRunResult.cs similarity index 75% rename from Source/ExecutionEngine/VerificationResult.cs rename to Source/ExecutionEngine/ImplementationRunResult.cs index 0a685c2fd..d0169164f 100644 --- a/Source/ExecutionEngine/VerificationResult.cs +++ b/Source/ExecutionEngine/ImplementationRunResult.cs @@ -7,7 +7,7 @@ namespace Microsoft.Boogie; -public sealed class VerificationResult +public sealed class ImplementationRunResult { private readonly Implementation implementation; public readonly string ProgramId; @@ -37,20 +37,20 @@ public int ProofObligationCount public int ProofObligationCountBefore { get; set; } public int ProofObligationCountAfter { get; set; } - public ConditionGeneration.Outcome Outcome { get; set; } + public VcOutcome VcOutcome { get; set; } public List Errors = new(); - public List VCResults; + public List VCResults; public ErrorInformation ErrorBeforeVerification { get; set; } - public VerificationResult(Implementation implementation, string programId = null) + public ImplementationRunResult(Implementation implementation, string programId = null) { this.implementation = implementation; ProgramId = programId; } public ErrorInformation GetOutcomeError(ExecutionEngineOptions options) { - return ExecutionEngine.GetOutcomeError(options, Outcome, implementation.VerboseName, implementation.tok, MessageIfVerifies, + return ExecutionEngine.GetOutcomeError(options, VcOutcome, implementation.VerboseName, implementation.tok, MessageIfVerifies, TextWriter.Null, implementation.GetTimeLimit(options), Errors); } @@ -62,11 +62,11 @@ public String GetOutput(OutputPrinter printer, printer.WriteErrorInformation(ErrorBeforeVerification, result); } - engine.ProcessOutcome(printer, Outcome, Errors, TimeIndication(engine.Options), stats, + engine.ProcessOutcome(printer, VcOutcome, Errors, TimeIndication(engine.Options), stats, result, implementation.GetTimeLimit(engine.Options), er, implementation.VerboseName, implementation.tok, MessageIfVerifies); - engine.ProcessErrors(printer, Errors, Outcome, result, er, implementation); + engine.ProcessErrors(printer, Errors, VcOutcome, result, er, implementation); return result.ToString(); } @@ -79,12 +79,12 @@ public void ProcessXml(ExecutionEngine engine) { lock (engine.Options.XmlSink) { engine.Options.XmlSink.WriteStartMethod(implementation.VerboseName, Start); - foreach (var vcResult in VCResults.OrderBy(s => (s.vcNum, s.iteration))) { - engine.Options.XmlSink.WriteSplit(vcResult.vcNum, vcResult.iteration, vcResult.asserts, vcResult.startTime, - vcResult.outcome.ToString().ToLowerInvariant(), vcResult.runTime, vcResult.resourceCount); + foreach (var vcResult in VCResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) { + engine.Options.XmlSink.WriteSplit(vcResult.VcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime, + vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount); } - engine.Options.XmlSink.WriteEndMethod(Outcome.ToString().ToLowerInvariant(), + engine.Options.XmlSink.WriteEndMethod(VcOutcome.ToString().ToLowerInvariant(), End, Elapsed, ResourceCount); } diff --git a/Source/ExecutionEngine/ImplementationTask.cs b/Source/ExecutionEngine/ImplementationTask.cs index 6badd42d0..26e385c9d 100644 --- a/Source/ExecutionEngine/ImplementationTask.cs +++ b/Source/ExecutionEngine/ImplementationTask.cs @@ -15,7 +15,7 @@ public interface IVerificationStatus {} /// /// Results are available /// -public record Completed(VerificationResult Result) : IVerificationStatus; +public record Completed(ImplementationRunResult Result) : IVerificationStatus; /// /// Scheduled to be run but waiting for resources @@ -32,7 +32,7 @@ public record Stale : IVerificationStatus; /// public record Running : IVerificationStatus; -public record BatchCompleted(Split Split, VCResult VcResult) : IVerificationStatus; +public record BatchCompleted(Split Split, VerificationRunResult VerificationRunResult) : IVerificationStatus; public interface IImplementationTask { IVerificationStatus CacheStatus { get; } diff --git a/Source/ExecutionEngine/OutputPrinter.cs b/Source/ExecutionEngine/OutputPrinter.cs index b24301561..527fc07e8 100644 --- a/Source/ExecutionEngine/OutputPrinter.cs +++ b/Source/ExecutionEngine/OutputPrinter.cs @@ -14,5 +14,5 @@ public interface OutputPrinter void WriteTrailer(TextWriter textWriter, PipelineStatistics stats); void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true); void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null); - void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result); + void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result); } diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index f03417e2b..1385c03d6 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -229,16 +229,16 @@ public static void Inject(ExecutionEngine engine, Program program, } private void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation, - VerificationResult result) + ImplementationRunResult result) { - if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null && + if (result.VcOutcome == VcOutcome.Errors && result.Errors != null && result.Errors.Count < options.ErrorLimit) { implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => new Tuple(cex.Checksum, cex.SugaredCmdChecksum, cex))); implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums; } - else if (result.Outcome == ConditionGeneration.Outcome.Correct) + else if (result.VcOutcome == VcOutcome.Correct) { implementation.SetErrorChecksumToCachedError(new List>()); implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums; @@ -690,7 +690,7 @@ public Program CachedProgram(string programId) { private readonly CacheItemPolicy Policy = new CacheItemPolicy {SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default}; - public void Insert(Implementation impl, VerificationResult result) + public void Insert(Implementation impl, ImplementationRunResult result) { Contract.Requires(impl != null); Contract.Requires(result != null); @@ -699,11 +699,11 @@ public void Insert(Implementation impl, VerificationResult result) } - public VerificationResult Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority) + public ImplementationRunResult Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority) { Contract.Requires(impl != null); - var result = Cache.Get(impl.Id) as VerificationResult; + var result = Cache.Get(impl.Id) as ImplementationRunResult; if (result == null) { priority = Priority.HIGH; @@ -716,7 +716,7 @@ public VerificationResult Lookup(Implementation impl, bool runDiagnosticsOnTimeo { priority = Priority.LOW; } - else if (result.Outcome == ConditionGeneration.Outcome.TimedOut && runDiagnosticsOnTimeout) + else if (result.VcOutcome == VcOutcome.TimedOut && runDiagnosticsOnTimeout) { priority = Priority.MEDIUM; } diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 9620b1889..5883784f9 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -52,7 +52,7 @@ public virtual void UpdateAssignment(Dictionary assignment) { } - public virtual void UpdateOutcome(ProverInterface.Outcome outcome) + public virtual void UpdateOutcome(Outcome outcome) { } @@ -158,7 +158,7 @@ public override void UpdateImplementation(Implementation implementation) curImp = implementation; } - public override void UpdateOutcome(ProverInterface.Outcome o) + public override void UpdateOutcome(Outcome o) { Contract.Assert(curImp != null); DateTime endT = DateTime.UtcNow; @@ -237,7 +237,7 @@ public override void UpdateAssignment(Dictionary assignment) wr.Flush(); } - public override void UpdateOutcome(ProverInterface.Outcome outcome) + public override void UpdateOutcome(Outcome outcome) { wr.WriteLine("analysis outcome :" + outcome); wr.Flush(); @@ -335,7 +335,7 @@ protected void NotifyAssignment(Dictionary assignment) Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); }); } - protected void NotifyOutcome(ProverInterface.Outcome outcome) + protected void NotifyOutcome(Outcome outcome) { Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); }); } @@ -837,13 +837,13 @@ protected Dictionary BuildAssignment(HashSet constants return initial; } - private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List errors) + private bool IsOutcomeNotHoudini(Outcome outcome, List errors) { switch (outcome) { - case ProverInterface.Outcome.Valid: + case Outcome.Valid: return false; - case ProverInterface.Outcome.Invalid: + case Outcome.Invalid: Contract.Assume(errors != null); foreach (Counterexample error in errors) { @@ -863,14 +863,14 @@ private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List errors) { string implName = implementation.Name; houdiniOutcome.implementationOutcomes.Remove(implName); List nonCandidateErrors = new List(); - if (outcome == ProverInterface.Outcome.Invalid) + if (outcome == Outcome.Invalid) { foreach (Counterexample error in errors) { @@ -937,7 +937,7 @@ protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) // Updates the worklist and current assignment // @return true if the current function is dequeued - protected bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome, + protected bool UpdateAssignmentWorkList(Outcome outcome, List errors) { Contract.Assume(currentHoudiniState.Implementation != null); @@ -945,11 +945,11 @@ protected bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome, switch (outcome) { - case ProverInterface.Outcome.Valid: + case Outcome.Valid: //yeah, dequeue break; - case ProverInterface.Outcome.Invalid: + case Outcome.Invalid: Contract.Assume(errors != null); foreach (Counterexample error in errors) @@ -1489,7 +1489,7 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) return null; } - private async Task<(ProverInterface.Outcome, List errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList completedStages) + private async Task<(Outcome, List errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList completedStages) { try { return await session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), GetErrorLimit()); @@ -1497,7 +1497,7 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) catch (UnexpectedProverOutputException upo) { Contract.Assume(upo != null); - return (ProverInterface.Outcome.Undetermined, null); + return (Outcome.Undetermined, null); } } @@ -1551,7 +1551,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead #region Explain Houdini - if (Options.ExplainHoudini && outcome == ProverInterface.Outcome.Invalid) + if (Options.ExplainHoudini && outcome == Outcome.Invalid) { Contract.Assume(errors != null); // make a copy of this variable @@ -1587,7 +1587,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead if (UpdateAssignmentWorkList(outcome, errors)) { - if (Options.UseUnsatCoreForContractInfer && outcome == ProverInterface.Outcome.Valid) + if (Options.UseUnsatCoreForContractInfer && outcome == Outcome.Valid) { await session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment); } @@ -1704,12 +1704,12 @@ public static void ApplyAssignment(Program prog, HoudiniOutcome outcome) public class VCGenOutcome { - public VCGen.Outcome outcome; + public VcOutcome VcOutcome; public List errors; - public VCGenOutcome(ProverInterface.Outcome outcome, List errors) + public VCGenOutcome(Outcome outcome, List errors) { - this.outcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome); + this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome); this.errors = errors; } } @@ -1724,12 +1724,12 @@ public class HoudiniOutcome // statistics - private int CountResults(VCGen.Outcome outcome) + private int CountResults(VcOutcome vcOutcome) { int outcomeCount = 0; foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) { - if (verifyOutcome.outcome == outcome) + if (verifyOutcome.VcOutcome == vcOutcome) { outcomeCount++; } @@ -1738,12 +1738,12 @@ private int CountResults(VCGen.Outcome outcome) return outcomeCount; } - private List ListOutcomeMatches(VCGen.Outcome outcome) + private List ListOutcomeMatches(VcOutcome vcOutcome) { List result = new List(); foreach (KeyValuePair kvpair in implementationOutcomes) { - if (kvpair.Value.outcome == outcome) + if (kvpair.Value.VcOutcome == vcOutcome) { result.Add(kvpair.Key); } @@ -1754,37 +1754,37 @@ private List ListOutcomeMatches(VCGen.Outcome outcome) public int ErrorCount { - get { return CountResults(VCGen.Outcome.Errors); } + get { return CountResults(VcOutcome.Errors); } } public int Verified { - get { return CountResults(VCGen.Outcome.Correct); } + get { return CountResults(VcOutcome.Correct); } } public int Inconclusives { - get { return CountResults(VCGen.Outcome.Inconclusive); } + get { return CountResults(VcOutcome.Inconclusive); } } public int TimeOuts { - get { return CountResults(VCGen.Outcome.TimedOut); } + get { return CountResults(VcOutcome.TimedOut); } } public List ListOfTimeouts { - get { return ListOutcomeMatches(VCGen.Outcome.TimedOut); } + get { return ListOutcomeMatches(VcOutcome.TimedOut); } } public List ListOfInconclusives { - get { return ListOutcomeMatches(VCGen.Outcome.Inconclusive); } + get { return ListOutcomeMatches(VcOutcome.Inconclusive); } } public List ListOfErrors { - get { return ListOutcomeMatches(VCGen.Outcome.Errors); } + get { return ListOutcomeMatches(VcOutcome.Errors); } } } } \ No newline at end of file diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 7603402d2..e4d0959c5 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -129,7 +129,7 @@ public class HoudiniStatistics public HashSet CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; - ConditionGeneration.VerificationResultCollector collector; + VerificationResultCollector collector; HashSet unsatCoreSet; HashSet houdiniConstants; public HashSet houdiniAssertConstants; @@ -163,7 +163,7 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf this.Description = impl.Name; this.houdini = houdini; this.stats = stats; - collector = new ConditionGeneration.VerificationResultCollector(houdini.Options); + collector = new VerificationResultCollector(houdini.Options); collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0); vcgen.ConvertCFG2DAG(run, taskID: taskID); @@ -252,7 +252,7 @@ private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary houdini.Options; - public async Task<(ProverInterface.Outcome, List errors)> Verify( + public async Task<(Outcome, List errors)> Verify( ProverInterface proverInterface, Dictionary assignment, int errorLimit) @@ -393,7 +393,7 @@ public async Task Explain(ProverInterface proverInterface, var el = Options.ErrorLimit; Options.ErrorLimit = 1; - var outcome = ProverInterface.Outcome.Undetermined; + var outcome = Outcome.Undetermined; do { @@ -402,8 +402,8 @@ public async Task Explain(ProverInterface proverInterface, handler, CancellationToken.None); hardAssumptions.RemoveAt(hardAssumptions.Count - 1); - if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || - outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.Outcome.Undetermined) + if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory || + outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined) { break; } @@ -436,8 +436,8 @@ public async Task Explain(ProverInterface proverInterface, (outcome, var unsatisfiedSoftAssumptions2) = await proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, handler, CancellationToken.None); - if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || - outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.Outcome.Undetermined) + if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory || + outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined) { break; } @@ -467,8 +467,8 @@ public async Task Explain(ProverInterface proverInterface, } } while (false); - if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || - outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.Outcome.Undetermined) + if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory || + outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined) { Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", Description); @@ -515,8 +515,8 @@ public async Task UpdateUnsatCore(ProverInterface proverInterface, Dictionary(); foreach (int i in unsatCore) { diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs index e50e23b73..ce2cea26d 100644 --- a/Source/Houdini/StagedHoudini.cs +++ b/Source/Houdini/StagedHoudini.cs @@ -6,6 +6,7 @@ using System.Threading.Tasks; using System.Threading; using Microsoft.Boogie.GraphUtil; +using VC; namespace Microsoft.Boogie.Houdini { @@ -308,8 +309,8 @@ private void EmitProgram(string filename) private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2) { - var vcOutcome1 = o1.outcome; - var vcOutcome2 = o2.outcome; + var vcOutcome1 = o1.VcOutcome; + var vcOutcome2 = o2.VcOutcome; if (vcOutcome1 == vcOutcome2) { @@ -317,34 +318,34 @@ private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2) } // Errors trump everything else - if (vcOutcome1 == VC.ConditionGeneration.Outcome.Errors) + if (vcOutcome1 == VcOutcome.Errors) { return o1; } - if (vcOutcome2 == VC.ConditionGeneration.Outcome.Errors) + if (vcOutcome2 == VcOutcome.Errors) { return o2; } // If one outcome is Correct, return the other in case it is "worse" - if (vcOutcome1 == VC.ConditionGeneration.Outcome.Correct) + if (vcOutcome1 == VcOutcome.Correct) { return o2; } - if (vcOutcome2 == VC.ConditionGeneration.Outcome.Correct) + if (vcOutcome2 == VcOutcome.Correct) { return o1; } // Neither outcome is correct, so if one outcome is ReachedBound, return the other in case it is "worse" - if (vcOutcome1 == VC.ConditionGeneration.Outcome.ReachedBound) + if (vcOutcome1 == VcOutcome.ReachedBound) { return o2; } - if (vcOutcome2 == VC.ConditionGeneration.Outcome.ReachedBound) + if (vcOutcome2 == VcOutcome.ReachedBound) { return o1; } diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index bad3f03f0..cad437a24 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -90,17 +90,6 @@ public static ProverInterface CreateProver(SMTLibOptions libOptions, Program pro return libOptions.TheProverFactory.SpawnProver(libOptions, options, ctx); } - public enum Outcome - { - Valid, - Invalid, - TimeOut, - OutOfMemory, - OutOfResource, - Undetermined, - Bounded - } - public readonly ISet NamedAssumes = new HashSet(); public class ErrorHandler @@ -305,6 +294,18 @@ public virtual void AssertNamed(VCExpr vc, bool polarity, string name) public abstract Task GoBackToIdle(); } + +public enum Outcome +{ + Valid, + Invalid, + TimeOut, + OutOfMemory, + OutOfResource, + Undetermined, + Bounded +} + public class UnexpectedProverOutputException : ProverException { public UnexpectedProverOutputException(string s) diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 26ee5dbd3..3ac3068df 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -71,7 +71,7 @@ procedure Second(y: int) Assert.NotNull(tasks[0].Implementation); var result1 = await tasks[0].TryRun()!.ToTask(); var verificationResult1 = ((Completed)result1).Result; - Assert.AreEqual(ConditionGeneration.Outcome.Errors, verificationResult1.Outcome); + Assert.AreEqual(VcOutcome.Errors, verificationResult1.VcOutcome); Assert.AreEqual(true, verificationResult1.Errors[0].Model.ModelHasStatesAlready); Assert.IsTrue(tasks[1].IsIdle); @@ -80,7 +80,7 @@ procedure Second(y: int) var result2 = await runningStates.ToTask(); Assert.IsTrue(tasks[1].IsIdle); var verificationResult2 = ((Completed)result2).Result; - Assert.AreEqual(ConditionGeneration.Outcome.Correct, verificationResult2.Outcome); + Assert.AreEqual(VcOutcome.Correct, verificationResult2.VcOutcome); } [Test] @@ -340,20 +340,20 @@ public async Task StatusTest() { var tasks2 = engine.GetImplementationTasks(program); Assert.True(tasks2[0].CacheStatus is Completed); - Assert.AreEqual(ConditionGeneration.Outcome.Errors, ((Completed)tasks2[0].CacheStatus).Result.Outcome); + Assert.AreEqual(VcOutcome.Errors, ((Completed)tasks2[0].CacheStatus).Result.VcOutcome); Assert.True(tasks2[1].CacheStatus is Completed); - Assert.AreEqual(ConditionGeneration.Outcome.Correct, ((Completed)tasks2[1].CacheStatus).Result.Outcome); + Assert.AreEqual(VcOutcome.Correct, ((Completed)tasks2[1].CacheStatus).Result.VcOutcome); var batchResult = (BatchCompleted) statusList[2].Item2; - var assertion = batchResult.VcResult.asserts[0]; - batchResult.VcResult.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExamples); + var assertion = batchResult.VerificationRunResult.Asserts[0]; + batchResult.VerificationRunResult.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExamples); Assert.Contains(assertion, perAssertOutcome.Keys); Assert.Contains(assertion, perAssertCounterExamples.Keys); var outcomeAssertion = perAssertOutcome[assertion]; var counterExampleAssertion = perAssertCounterExamples[assertion]; - Assert.AreEqual(ProverInterface.Outcome.Invalid, outcomeAssertion); + Assert.AreEqual(Outcome.Invalid, outcomeAssertion); Assert.AreEqual(true, counterExampleAssertion is AssertCounterexample); var assertCounterexample = (AssertCounterexample)counterExampleAssertion; Assert.AreEqual(assertCounterexample.FailingAssert, assertion); @@ -374,10 +374,10 @@ public async Task SolverCrash() options.VcsCores = 1; var outcome1 = await executionEngine.GetImplementationTasks(terminatingProgram)[0].TryRun()!.ToTask(); - Assert.IsTrue(outcome1 is Completed completed && completed.Result.Outcome == ConditionGeneration.Outcome.Inconclusive); + Assert.IsTrue(outcome1 is Completed completed && completed.Result.VcOutcome == VcOutcome.Inconclusive); options.CreateSolver = (_ ,_ ) => new UnsatSolver(); var outcome2 = await executionEngine.GetImplementationTasks(terminatingProgram)[0].TryRun()!.ToTask(); - Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.Outcome == ConditionGeneration.Outcome.Correct); + Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.VcOutcome == VcOutcome.Correct); } [Test] diff --git a/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs b/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs index 99175bb0a..d14791b30 100644 --- a/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs +++ b/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs @@ -30,7 +30,7 @@ public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, boo public void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { } - public void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) + public void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) { } } diff --git a/Source/VCGeneration/BlockListComparer.cs b/Source/VCGeneration/BlockListComparer.cs new file mode 100644 index 000000000..3df87811c --- /dev/null +++ b/Source/VCGeneration/BlockListComparer.cs @@ -0,0 +1,29 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; + +namespace VC; + +class BlockListComparer : IEqualityComparer> +{ + public bool Equals(List x, List y) + { + return x == y || x.SequenceEqual(y); + } + + public int GetHashCode(List obj) + { + int h = 0; + Contract.Assume(obj != null); + foreach (var b in obj) + { + if (b != null) + { + h += b.GetHashCode(); + } + } + + return h; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/BlockStats.cs b/Source/VCGeneration/BlockStats.cs new file mode 100644 index 000000000..eba08b349 --- /dev/null +++ b/Source/VCGeneration/BlockStats.cs @@ -0,0 +1,40 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Boogie; + +namespace VC; + +class BlockStats +{ + public bool bigBlock; + public int id; + public double assertionCost; + public double assumptionCost; // before multiplier + public double incomingPaths; + + public List /*!>!*/ + virtualSuccessors = new List(); + + public List /*!>!*/ + virtualPredecessors = new List(); + + public HashSet reachableBlocks; + public readonly Block block; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(cce.NonNullElements(virtualSuccessors)); + Contract.Invariant(cce.NonNullElements(virtualPredecessors)); + Contract.Invariant(block != null); + } + + + public BlockStats(Block b, int i) + { + Contract.Requires(b != null); + block = b; + assertionCost = -1; + id = i; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs new file mode 100644 index 000000000..89f17aac7 --- /dev/null +++ b/Source/VCGeneration/BlockTransformations.cs @@ -0,0 +1,64 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; + +namespace VCGeneration; + +public static class BlockTransformations +{ + public static List PostProcess(List blocks) + { + void DeleteFalseGotos (Block b) + { + var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse); + if (firstFalseIdx != -1) + { + b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList(); + b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd; + } + + return; + + bool IsAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; } + } + + bool ContainsAssert(Block b) + { + return b.Cmds.Exists(IsNonTrivialAssert); + bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } + } + + blocks.ForEach(DeleteFalseGotos); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously + var todo = new Stack(); + var peeked = new HashSet(); + var interestingBlocks = new HashSet(); + todo.Push(blocks[0]); + while(todo.Any()) + { + var currentBlock = todo.Peek(); + var pop = peeked.Contains(currentBlock); + peeked.Add(currentBlock); + var interesting = false; + var exit = currentBlock.TransferCmd as GotoCmd; + if (exit != null && !pop) { + exit.labelTargets.ForEach(b => todo.Push(b)); + } else if (exit != null) { + Contract.Assert(pop); + var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); + currentBlock.TransferCmd = gtc; + interesting = interesting || gtc.labelTargets.Count() != 0; + } + if (pop) + { + interesting = interesting || ContainsAssert(currentBlock); + if (interesting) { + interestingBlocks.Add(currentBlock); + } + todo.Pop(); + } + } + interestingBlocks.Add(blocks[0]); // must not be empty + return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. + } +} \ No newline at end of file diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index f5f8c2f8d..6ce4cc4cc 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -40,7 +40,7 @@ void ObjectInvariant() private ProverInterface thmProver; // state for the async interface - private volatile ProverInterface.Outcome outcome; + private volatile Outcome outcome; private volatile bool hasOutput; private volatile UnexpectedProverOutputException outputExn; public DateTime ProverStart { get; private set; } @@ -292,22 +292,22 @@ private async Task Check(string descriptiveName, VCExpr vc, CancellationToken ca switch (outcome) { - case ProverInterface.Outcome.Valid: + case Outcome.Valid: thmProver.LogComment("Valid"); break; - case ProverInterface.Outcome.Invalid: + case Outcome.Invalid: thmProver.LogComment("Invalid"); break; - case ProverInterface.Outcome.TimeOut: + case Outcome.TimeOut: thmProver.LogComment("Timed out"); break; - case ProverInterface.Outcome.OutOfResource: + case Outcome.OutOfResource: thmProver.LogComment("Out of resource"); break; - case ProverInterface.Outcome.OutOfMemory: + case Outcome.OutOfMemory: thmProver.LogComment("Out of memory"); break; - case ProverInterface.Outcome.Undetermined: + case Outcome.Undetermined: thmProver.LogComment("Undetermined"); break; } @@ -341,7 +341,7 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface. ProverTask = Check(descriptiveName, vc, cancellationToken); } - public ProverInterface.Outcome ReadOutcome() + public Outcome ReadOutcome() { Contract.Requires(IsBusy); Contract.Requires(HasOutput); diff --git a/Source/VCGeneration/CommandTransformations.cs b/Source/VCGeneration/CommandTransformations.cs new file mode 100644 index 000000000..a39bac235 --- /dev/null +++ b/Source/VCGeneration/CommandTransformations.cs @@ -0,0 +1,17 @@ +using Microsoft.Boogie; +using VC; + +namespace VCGeneration; + +public class CommandTransformations +{ + public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c) + { + if (c is AssertCmd assrt) + { + return VCGen.AssertTurnedIntoAssume(options, assrt); + } + + return c; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index d9d900377..418d47198 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1,7 +1,6 @@ using System; using System.Linq; using System.Collections; -using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics; using System.Threading; @@ -27,8 +26,8 @@ public VCGenException(string s) [ContractClassFor(typeof(ConditionGeneration))] public abstract class ConditionGenerationContracts : ConditionGeneration { - public override Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, - CancellationToken cancellationToken, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver) + public override Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, + CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver) { Contract.Requires(run != null); Contract.Requires(callback != null); @@ -45,37 +44,25 @@ public ConditionGenerationContracts(Program program, CheckerPool checkerPool) [ContractClass(typeof(ConditionGenerationContracts))] public abstract class ConditionGeneration : IDisposable { - public enum Outcome - { - Correct, - Errors, - TimedOut, - OutOfResource, - OutOfMemory, - Inconclusive, - ReachedBound, - SolverException - } - - public static Outcome ProverInterfaceOutcomeToConditionGenerationOutcome(ProverInterface.Outcome outcome) + public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Microsoft.Boogie.Outcome outcome) { switch (outcome) { - case ProverInterface.Outcome.Invalid: - return Outcome.Errors; - case ProverInterface.Outcome.OutOfMemory: - return Outcome.OutOfMemory; - case ProverInterface.Outcome.TimeOut: - return Outcome.TimedOut; - case ProverInterface.Outcome.OutOfResource: - return Outcome.OutOfResource; - case ProverInterface.Outcome.Undetermined: - return Outcome.Inconclusive; - case ProverInterface.Outcome.Valid: - return Outcome.Correct; + case Microsoft.Boogie.Outcome.Invalid: + return VcOutcome.Errors; + case Microsoft.Boogie.Outcome.OutOfMemory: + return VcOutcome.OutOfMemory; + case Microsoft.Boogie.Outcome.TimeOut: + return VcOutcome.TimedOut; + case Microsoft.Boogie.Outcome.OutOfResource: + return VcOutcome.OutOfResource; + case Microsoft.Boogie.Outcome.Undetermined: + return VcOutcome.Inconclusive; + case Microsoft.Boogie.Outcome.Valid: + return VcOutcome.Correct; } - return Outcome.Inconclusive; // unreachable but the stupid compiler does not understand + return VcOutcome.Inconclusive; // unreachable but the stupid compiler does not understand } [ContractInvariantMethod] @@ -120,8 +107,8 @@ public ConditionGeneration(Program program, CheckerPool checkerPool) /// /// /// - public async Task<(Outcome, List errors, List vcResults)> VerifyImplementation( - ImplementationRun run, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver, + public async Task<(VcOutcome, List errors, List vcResults)> VerifyImplementation( + ImplementationRun run, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver, CancellationToken cancellationToken) { Contract.Requires(run != null); @@ -130,21 +117,21 @@ public ConditionGeneration(Program program, CheckerPool checkerPool) Helpers.ExtraTraceInformation(Options, "Starting implementation verification"); var collector = new VerificationResultCollector(Options); - Outcome outcome = await VerifyImplementation(run, collector, cancellationToken, batchCompletedObserver); + VcOutcome vcOutcome = await VerifyImplementation(run, collector, cancellationToken, batchCompletedObserver); var /*?*/ errors = new List(); - if (outcome == Outcome.Errors || outcome == Outcome.TimedOut || outcome == Outcome.OutOfMemory || - outcome == Outcome.OutOfResource) { + if (vcOutcome == VcOutcome.Errors || vcOutcome == VcOutcome.TimedOut || vcOutcome == VcOutcome.OutOfMemory || + vcOutcome == VcOutcome.OutOfResource) { errors = collector.examples.ToList(); } Helpers.ExtraTraceInformation(Options, "Finished implementation verification"); - return (outcome, errors, collector.vcResults.ToList()); + return (vcOutcome, errors, collector.vcResults.ToList()); } private VCGenOptions Options => CheckerPool.Options; - public abstract Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, - CancellationToken cancellationToken, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver); + public abstract Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, + CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver); /////////////////////////////////// Common Methods and Classes ////////////////////////////////////////// @@ -523,46 +510,6 @@ public virtual void Close() } - public class VerificationResultCollector : VerifierCallback - { - private readonly VCGenOptions options; - - public VerificationResultCollector(VCGenOptions options) : base(options.PrintProverWarnings) - { - this.options = options; - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(examples)); - Contract.Invariant(cce.NonNullElements(vcResults)); - } - - public readonly ConcurrentQueue examples = new(); - public readonly ConcurrentQueue vcResults = new(); - - public override void OnCounterexample(Counterexample ce, string /*?*/ reason) - { - //Contract.Requires(ce != null); - ce.InitializeModelStates(); - examples.Enqueue(ce); - } - - public override void OnUnreachableCode(ImplementationRun run) - { - //Contract.Requires(impl != null); - run.OutputWriter.WriteLine("found unreachable code:"); - EmitImpl(options, run, false); - // TODO report error about next to last in seq - } - - public override void OnVCResult(VCResult result) - { - vcResults.Enqueue(result); - } - } - public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool printDesugarings) { var impl = run.Implementation; @@ -1662,6 +1609,18 @@ protected virtual void Dispose(bool disposing) } } + public enum VcOutcome + { + Correct, + Errors, + TimedOut, + OutOfResource, + OutOfMemory, + Inconclusive, + ReachedBound, + SolverException + } + public record ImplementationRun(Implementation Implementation, TextWriter OutputWriter) { } diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs index e48d0c1fa..457568fdd 100644 --- a/Source/VCGeneration/Counterexample.cs +++ b/Source/VCGeneration/Counterexample.cs @@ -388,14 +388,14 @@ public Model.Element GetModelValue(Variable v) public abstract int GetLocation(); - public ErrorInformation CreateErrorInformation(ConditionGeneration.Outcome outcome, bool forceBplErrors) + public ErrorInformation CreateErrorInformation(VcOutcome vcOutcome, bool forceBplErrors) { ErrorInformation errorInfo; - var cause = outcome switch { - VCGen.Outcome.TimedOut => "Timed out on", - VCGen.Outcome.OutOfMemory => "Out of memory on", - VCGen.Outcome.SolverException => "Solver exception on", - VCGen.Outcome.OutOfResource => "Out of resource on", + var cause = vcOutcome switch { + VcOutcome.TimedOut => "Timed out on", + VcOutcome.OutOfMemory => "Out of memory on", + VcOutcome.SolverException => "Solver exception on", + VcOutcome.OutOfResource => "Out of resource on", _ => "Error" }; @@ -766,7 +766,7 @@ public virtual void OnWarning(CoreOptions options, string msg) } } - public virtual void OnVCResult(VCResult result) + public virtual void OnVCResult(VerificationRunResult result) { Contract.Requires(result != null); } diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs new file mode 100644 index 000000000..e08874579 --- /dev/null +++ b/Source/VCGeneration/FocusAttribute.cs @@ -0,0 +1,139 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; +using VC; +using Block = Microsoft.Boogie.Block; +using Cmd = Microsoft.Boogie.Cmd; +using PredicateCmd = Microsoft.Boogie.PredicateCmd; +using QKeyValue = Microsoft.Boogie.QKeyValue; +using ReturnCmd = Microsoft.Boogie.ReturnCmd; +using TransferCmd = Microsoft.Boogie.TransferCmd; +using VCGenOptions = Microsoft.Boogie.VCGenOptions; + +namespace VCGeneration; + +public static class FocusAttribute +{ + public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par) + { + bool IsFocusCmd(Cmd c) { + return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); + } + + List GetFocusBlocks(List blocks) { + return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList(); + } + + var impl = run.Implementation; + var dag = Program.GraphFromImpl(impl); + var topoSorted = dag.TopologicalSort().ToList(); + // By default, we process the foci in a top-down fashion, i.e., in the topological order. + // If the user sets the RelaxFocus flag, we use the reverse (topological) order. + var focusBlocks = GetFocusBlocks(topoSorted); + if (par.CheckerPool.Options.RelaxFocus) { + focusBlocks.Reverse(); + } + if (!focusBlocks.Any()) { + var f = new List(); + f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run)); + return f; + } + // finds all the blocks dominated by focusBlock in the subgraph + // which only contains vertices of subgraph. + HashSet DominatedBlocks(Block focusBlock, IEnumerable subgraph) + { + var dominators = new Dictionary>(); + var todo = new Queue(); + foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk))) + { + var s = new HashSet(); + var pred = b.Predecessors.Where(subgraph.Contains).ToList(); + if (pred.Count != 0) + { + s.UnionWith(dominators[pred[0]]); + pred.ForEach(blk => s.IntersectWith(dominators[blk])); + } + s.Add(b); + dominators[b] = s; + } + return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet(); + } + + Cmd DisableSplits(Cmd c) + { + if (c is PredicateCmd pc) + { + for (var kv = pc.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == "split") + { + kv.AddParam(new LiteralExpr(Token.NoToken, false)); + } + } + } + return c; + } + + var Ancestors = new Dictionary>(); + var Descendants = new Dictionary>(); + focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet()); + focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet()); + var s = new List(); + var duplicator = new Duplicator(); + void FocusRec(int focusIdx, IEnumerable blocks, IEnumerable freeBlocks) + { + if (focusIdx == focusBlocks.Count()) + { + // it is important for l to be consistent with reverse topological order. + var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse(); + // assert that the root block, impl.Blocks[0], is in l + Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]); + var newBlocks = new List(); + var oldToNewBlockMap = new Dictionary(blocks.Count()); + foreach (Block b in l) + { + var newBlock = (Block)duplicator.Visit(b); + newBlocks.Add(newBlock); + oldToNewBlockMap[b] = newBlock; + // freeBlocks consist of the predecessors of the relevant foci. + // Their assertions turn into assumes and any splits inside them are disabled. + if(freeBlocks.Contains(b)) + { + newBlock.Cmds = b.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList(); + } + if (b.TransferCmd is GotoCmd gtc) + { + var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk)); + newBlock.TransferCmd = new GotoCmd(gtc.tok, + targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), + targets.Select(blk => oldToNewBlockMap[blk]).ToList()); + } + } + newBlocks.Reverse(); + Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]); + s.Add(new Split(options, BlockTransformations.PostProcess(newBlocks), gotoCmdOrigins, par, run)); + } + else if (!blocks.Contains(focusBlocks[focusIdx]) + || freeBlocks.Contains(focusBlocks[focusIdx])) + { + FocusRec(focusIdx + 1, blocks, freeBlocks); + } + else + { + var b = focusBlocks[focusIdx]; // assert b in blocks + var dominatedBlocks = DominatedBlocks(b, blocks); + // the first part takes all blocks except the ones dominated by the focus block + FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks); + var ancestors = Ancestors[b]; + ancestors.Remove(b); + var descendants = Descendants[b]; + // the other part takes all the ancestors, the focus block, and the descendants. + FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks)); + } + } + + FocusRec(0, impl.Blocks, new List()); + return s; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs new file mode 100644 index 000000000..76c3922d6 --- /dev/null +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -0,0 +1,167 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; +using VC; + +namespace VCGeneration; + +public static class ManualSplitFinder +{ + + public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par, bool splitOnEveryAssert) + { + List focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); + var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList(); + return splits; + } + + public static List FindManualSplits(Split initialSplit, bool splitOnEveryAssert) + { + Contract.Requires(initialSplit.Implementation != null); + Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); + + var splitPoints = new Dictionary(); + foreach (var b in initialSplit.Blocks) + { + foreach (Cmd c in b.Cmds) + { + var p = c as PredicateCmd; + if (ShouldSplitHere(c, splitOnEveryAssert)) + { + splitPoints.TryGetValue(b, out var count); + splitPoints[b] = count + 1; + } + } + } + var splits = new List(); + if (!splitPoints.Any()) + { + splits.Add(initialSplit); + } + else + { + Block entryPoint = initialSplit.Blocks[0]; + var blockAssignments = PickBlocksToVerify(initialSplit.Blocks, splitPoints); + var entryBlockHasSplit = splitPoints.Keys.Contains(entryPoint); + var baseSplitBlocks = BlockTransformations.PostProcess(DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert)); + splits.Add(new Split(initialSplit.Options, baseSplitBlocks, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); + foreach (KeyValuePair pair in splitPoints) + { + for (int i = 0; i < pair.Value; i++) + { + bool lastSplitInBlock = i == pair.Value - 1; + var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert); + splits.Add(new Split(initialSplit.Options, BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); // REVIEW: Does gotoCmdOrigins need to be changed at all? + } + } + } + return splits; + } + + private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) { + return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here") + || c is AssertCmd && splitOnEveryAssert; + } + + + // Verify b with the last split in blockAssignments[b] + + private static Dictionary PickBlocksToVerify (List blocks, Dictionary splitPoints) + { + var todo = new Stack(); + var blockAssignments = new Dictionary(); + var immediateDominator = (Program.GraphFromBlocks(blocks)).ImmediateDominator(); + todo.Push(blocks[0]); + while(todo.Count > 0) + { + var currentBlock = todo.Pop(); + if (blockAssignments.Keys.Contains(currentBlock)) + { + continue; + } + else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. + { + blockAssignments[currentBlock] = currentBlock; + } + else if (splitPoints.Keys.Contains(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split + { + blockAssignments[currentBlock] = immediateDominator[currentBlock]; + } + else + { + Contract.Assert(blockAssignments.Keys.Contains(immediateDominator[currentBlock])); + blockAssignments[currentBlock] = blockAssignments[immediateDominator[currentBlock]]; + } + if (currentBlock.TransferCmd is GotoCmd exit) + { + exit.labelTargets.ForEach(blk => todo.Push(blk)); + } + } + return blockAssignments; + } + + private static List DoPreAssignedManualSplit(VCGenOptions options, List blocks, Dictionary blockAssignments, int splitNumberWithinBlock, + Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) + { + var newBlocks = new List(blocks.Count()); // Copies of the original blocks + var duplicator = new Duplicator(); + var oldToNewBlockMap = new Dictionary(blocks.Count()); // Maps original blocks to their new copies in newBlocks + foreach (var currentBlock in blocks) + { + var newBlock = (Block)duplicator.VisitBlock(currentBlock); + oldToNewBlockMap[currentBlock] = newBlock; + newBlocks.Add(newBlock); + if (currentBlock == containingBlock) + { + var newCmds = new List(); + var splitCount = -1; + var verify = splitCount == splitNumberWithinBlock; + foreach (Cmd c in currentBlock.Cmds) + { + if (ShouldSplitHere(c, splitOnEveryAssert)) + { + splitCount++; + verify = splitCount == splitNumberWithinBlock; + } + newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c)); + } + newBlock.Cmds = newCmds; + } + else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) + { + var verify = true; + var newCmds = new List(); + foreach(Cmd c in currentBlock.Cmds) { + verify = !ShouldSplitHere(c, splitOnEveryAssert) && verify; + newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c)); + } + newBlock.Cmds = newCmds; + } + else + { + newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList(); + } + } + // Patch the edges between the new blocks + foreach (var oldBlock in blocks) + { + if (oldBlock.TransferCmd is ReturnCmd) + { + continue; + } + + var gotoCmd = (GotoCmd)oldBlock.TransferCmd; + var newLabelTargets = new List(gotoCmd.labelTargets.Count()); + var newLabelNames = new List(gotoCmd.labelTargets.Count()); + foreach (var target in gotoCmd.labelTargets) + { + newLabelTargets.Add(oldToNewBlockMap[target]); + newLabelNames.Add(oldToNewBlockMap[target].Label); + } + + oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets); + } + return newBlocks; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index f449cce68..432236303 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -278,7 +278,7 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s Checker checker = await parent.CheckerPool.FindCheckerFor(parent, null, CancellationToken.None); Contract.Assert(checker != null); - ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined; + Outcome outcome = Outcome.Undetermined; try { VCExpr vc; @@ -327,12 +327,12 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s if (Options.Trace) { traceWriter.WriteLine(" [{0} s] {1}", elapsed.TotalSeconds, - outcome == ProverInterface.Outcome.Valid + outcome == Outcome.Valid ? "OOPS" - : "OK" + (outcome == ProverInterface.Outcome.Invalid ? "" : " (" + outcome + ")")); + : "OK" + (outcome == Outcome.Invalid ? "" : " (" + outcome + ")")); } - if (outcome == ProverInterface.Outcome.Valid) + if (outcome == Outcome.Valid) { // copy it again, so we get the version with calls, assignments and such copy = CopyBlock(cur); diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 460a2acdc..e6fb880d7 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -9,6 +9,7 @@ using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; +using VCGeneration; namespace VC { @@ -17,56 +18,21 @@ namespace VC public class Split : ProofRun { - private VCGenOptions options; + public VCGenOptions Options { get; } - public int? RandomSeed => Implementation.RandomSeed ?? options.RandomSeed; - private Random randomGen; + public int? RandomSeed => Implementation.RandomSeed ?? Options.RandomSeed; + private readonly Random randomGen; - private ImplementationRun run; - - class BlockStats - { - public bool bigBlock; - public int id; - public double assertionCost; - public double assumptionCost; // before multiplier - public double incomingPaths; - - public List /*!>!*/ - virtualSuccessors = new List(); - - public List /*!>!*/ - virtualPredecessors = new List(); - - public HashSet reachableBlocks; - public readonly Block block; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(virtualSuccessors)); - Contract.Invariant(cce.NonNullElements(virtualPredecessors)); - Contract.Invariant(block != null); - } - - - public BlockStats(Block b, int i) - { - Contract.Requires(b != null); - block = b; - assertionCost = -1; - id = i; - } - } + public ImplementationRun Run { get; } [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(blocks)); + Contract.Invariant(cce.NonNullElements(Blocks)); Contract.Invariant(cce.NonNullElements(bigBlocks)); Contract.Invariant(cce.NonNullDictionaryAndValues(stats)); Contract.Invariant(cce.NonNullElements(assumizedBranches)); - Contract.Invariant(gotoCmdOrigins != null); + Contract.Invariant(GotoCmdOrigins != null); Contract.Invariant(parent != null); Contract.Invariant(Implementation != null); Contract.Invariant(copies != null); @@ -75,8 +41,8 @@ void ObjectInvariant() } - private readonly List blocks; - public List Asserts => blocks.SelectMany(block => block.cmds.OfType()).ToList(); + public List Blocks { get; } + public List Asserts => Blocks.SelectMany(block => block.cmds.OfType()).ToList(); public readonly IReadOnlyList TopLevelDeclarations; readonly List bigBlocks = new(); @@ -96,13 +62,11 @@ void ObjectInvariant() int assertionCount; double assertionCost; // without multiplication by paths - Dictionary /*!*/ - gotoCmdOrigins; + public Dictionary GotoCmdOrigins { get; } - readonly public VCGen /*!*/ - parent; + public readonly VCGen /*!*/ parent; - public Implementation /*!*/ Implementation => run.Implementation; + public Implementation /*!*/ Implementation => Run.Implementation; Dictionary /*!*/ copies = new Dictionary(); @@ -129,11 +93,11 @@ public Split(VCGenOptions options, List /*!*/ blocks, Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(gotoCmdOrigins != null); Contract.Requires(par != null); - this.blocks = blocks; - this.gotoCmdOrigins = gotoCmdOrigins; + this.Blocks = blocks; + this.GotoCmdOrigins = gotoCmdOrigins; this.parent = par; - this.run = run; - this.options = options; + this.Run = run; + this.Options = options; Interlocked.Increment(ref currentId); TopLevelDeclarations = par.program.TopLevelDeclarations; @@ -145,14 +109,14 @@ public Split(VCGenOptions options, List /*!*/ blocks, private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix) { - if (!options.Prune || options.PrintPrunedFile == null) + if (!Options.Prune || Options.PrintPrunedFile == null) { return; } using var writer = new TokenTextWriter( - $"{options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, - options.PrettyPrint, options); + $"{Options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, + Options.PrettyPrint, Options); var functionAxioms = program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); @@ -230,17 +194,17 @@ public void DumpDot(int splitNum) string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum); using (System.IO.StreamWriter sw = System.IO.File.CreateText(filename)) { - int oldPrintUnstructured = options.PrintUnstructured; - options.PrintUnstructured = 2; // print only the unstructured program - bool oldPrintDesugaringSetting = options.PrintDesugarings; - options.PrintDesugarings = false; + int oldPrintUnstructured = Options.PrintUnstructured; + Options.PrintUnstructured = 2; // print only the unstructured program + bool oldPrintDesugaringSetting = Options.PrintDesugarings; + Options.PrintDesugarings = false; List backup = Implementation.Blocks; Contract.Assert(backup != null); - Implementation.Blocks = blocks; - Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, options), 0); + Implementation.Blocks = Blocks; + Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, Options), 0); Implementation.Blocks = backup; - options.PrintDesugarings = oldPrintDesugaringSetting; - options.PrintUnstructured = oldPrintUnstructured; + Options.PrintDesugarings = oldPrintDesugaringSetting; + Options.PrintUnstructured = oldPrintUnstructured; } } @@ -357,13 +321,13 @@ void ComputeBestSplit() assertionCount = 0; - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); CountAssertions(b); } - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); BlockStats bs = GetBlockStats(b); @@ -376,7 +340,7 @@ void ComputeBestSplit() BlockStats chs = GetBlockStats(ch); if (!chs.bigBlock) { - options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b); + Options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b); DumpDot(-1); Contract.Assert(false); throw new cce.UnreachableException(); @@ -446,7 +410,7 @@ void ComputeBestSplit() } } - if (options.VcsPathSplitMult * score > totalCost) + if (Options.VcsPathSplitMult * score > totalCost) { splitBlock = null; score = -1; @@ -485,7 +449,7 @@ void UpdateIncommingPaths(BlockStats s) if (count > 1) { - s.incomingPaths *= options.VcsPathJoinMult; + s.incomingPaths *= Options.VcsPathJoinMult; } } } @@ -534,11 +498,11 @@ void ComputeBlockSets(bool allowSmall) keepAtAll.Clear(); Debug.Assert(splitBlock == null || GetBlockStats(splitBlock).bigBlock); - Debug.Assert(GetBlockStats(blocks[0]).bigBlock); + Debug.Assert(GetBlockStats(Blocks[0]).bigBlock); if (assertToAssume) { - foreach (Block b in allowSmall ? blocks : bigBlocks) + foreach (Block b in allowSmall ? Blocks : bigBlocks) { Contract.Assert(b != null); if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock))) @@ -563,7 +527,7 @@ void ComputeBlockSets(bool allowSmall) } else { - ComputeBlockSetsHelper(blocks[0], allowSmall); + ComputeBlockSetsHelper(Blocks[0], allowSmall); } } @@ -584,7 +548,7 @@ double DoComputeScore(bool aa) GetBlockStats(b).incomingPaths = -1.0; } - GetBlockStats(blocks[0]).incomingPaths = 1.0; + GetBlockStats(Blocks[0]).incomingPaths = 1.0; double cost = 0.0; foreach (Block b in bigBlocks) @@ -597,14 +561,14 @@ double DoComputeScore(bool aa) double local = s.assertionCost; if (ShouldAssumize(b)) { - local = (s.assertionCost + s.assumptionCost) * options.VcsAssumeMult; + local = (s.assertionCost + s.assumptionCost) * Options.VcsAssumeMult; } else { - local = s.assumptionCost * options.VcsAssumeMult + s.assertionCost; + local = s.assumptionCost * Options.VcsAssumeMult + s.assertionCost; } - local = local + local * s.incomingPaths * options.VcsPathCostMult; + local = local + local * s.incomingPaths * Options.VcsPathCostMult; cost += local; } } @@ -652,7 +616,7 @@ List SliceCmds(Block b) if (swap) { - theNewCmd = VCGen.AssertTurnedIntoAssume(options, a); + theNewCmd = VCGen.AssertTurnedIntoAssume(Options, a); } } @@ -704,18 +668,18 @@ Split DoSplit() Contract.Ensures(Contract.Result() != null); copies.Clear(); - CloneBlock(blocks[0]); + CloneBlock(Blocks[0]); List newBlocks = new List(); Dictionary newGotoCmdOrigins = new Dictionary(); - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); if (copies.TryGetValue(b, out var tmp)) { newBlocks.Add(cce.NonNull(tmp)); - if (gotoCmdOrigins.ContainsKey(b.TransferCmd)) + if (GotoCmdOrigins.ContainsKey(b.TransferCmd)) { - newGotoCmdOrigins[tmp.TransferCmd] = gotoCmdOrigins[b.TransferCmd]; + newGotoCmdOrigins[tmp.TransferCmd] = GotoCmdOrigins[b.TransferCmd]; } foreach (Block p in b.Predecessors) @@ -729,7 +693,7 @@ Split DoSplit() } } - return new Split(options, newBlocks, newGotoCmdOrigins, parent, run); + return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run); } Split SplitAt(int idx) @@ -767,8 +731,8 @@ void Print() { List tmp = Implementation.Blocks; Contract.Assert(tmp != null); - Implementation.Blocks = blocks; - ConditionGeneration.EmitImpl(options, run, false); + Implementation.Blocks = Blocks; + ConditionGeneration.EmitImpl(Options, Run, false); Implementation.Blocks = tmp; } @@ -778,13 +742,13 @@ public Counterexample ToCounterexample(ProverContext context) Contract.Ensures(Contract.Result() != null); List trace = new List(); - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); trace.Add(b); } - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); foreach (Cmd c in b.Cmds) @@ -792,7 +756,7 @@ public Counterexample ToCounterexample(ProverContext context) Contract.Assert(c != null); if (c is AssertCmd) { - var counterexample = VCGen.AssertCmdToCounterexample(options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this); + var counterexample = VCGen.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this); Counterexamples.Add(counterexample); return counterexample; } @@ -803,339 +767,12 @@ public Counterexample ToCounterexample(ProverContext context) throw new cce.UnreachableException(); } - // Verify b with the last split in blockAssignments[b] - private static Dictionary PickBlocksToVerify (List blocks, Dictionary splitPoints) - { - var todo = new Stack(); - var blockAssignments = new Dictionary(); - var immediateDominator = (Program.GraphFromBlocks(blocks)).ImmediateDominator(); - todo.Push(blocks[0]); - while(todo.Count > 0) - { - var currentBlock = todo.Pop(); - if (blockAssignments.Keys.Contains(currentBlock)) - { - continue; - } - else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. - { - blockAssignments[currentBlock] = currentBlock; - } - else if (splitPoints.Keys.Contains(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split - { - blockAssignments[currentBlock] = immediateDominator[currentBlock]; - } - else - { - Contract.Assert(blockAssignments.Keys.Contains(immediateDominator[currentBlock])); - blockAssignments[currentBlock] = blockAssignments[immediateDominator[currentBlock]]; - } - if (currentBlock.TransferCmd is GotoCmd exit) - { - exit.labelTargets.ForEach(blk => todo.Push(blk)); - } - } - return blockAssignments; - } - private static List DoPreAssignedManualSplit(VCGenOptions options, List blocks, Dictionary blockAssignments, int splitNumberWithinBlock, - Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) - { - var newBlocks = new List(blocks.Count()); // Copies of the original blocks - var duplicator = new Duplicator(); - var oldToNewBlockMap = new Dictionary(blocks.Count()); // Maps original blocks to their new copies in newBlocks - foreach (var currentBlock in blocks) - { - var newBlock = (Block)duplicator.VisitBlock(currentBlock); - oldToNewBlockMap[currentBlock] = newBlock; - newBlocks.Add(newBlock); - if (currentBlock == containingBlock) - { - var newCmds = new List(); - var splitCount = -1; - var verify = splitCount == splitNumberWithinBlock; - foreach (Cmd c in currentBlock.Cmds) - { - if (ShouldSplitHere(c, splitOnEveryAssert)) - { - splitCount++; - verify = splitCount == splitNumberWithinBlock; - } - newCmds.Add(verify ? c : AssertIntoAssume(options, c)); - } - newBlock.Cmds = newCmds; - } - else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) - { - var verify = true; - var newCmds = new List(); - foreach(Cmd c in currentBlock.Cmds) { - verify = !ShouldSplitHere(c, splitOnEveryAssert) && verify; - newCmds.Add(verify ? c : AssertIntoAssume(options, c)); - } - newBlock.Cmds = newCmds; - } - else - { - newBlock.Cmds = currentBlock.Cmds.Select(x => AssertIntoAssume(options, x)).ToList(); - } - } - // Patch the edges between the new blocks - foreach (var oldBlock in blocks) - { - if (oldBlock.TransferCmd is ReturnCmd) - { - continue; - } - - var gotoCmd = (GotoCmd)oldBlock.TransferCmd; - var newLabelTargets = new List(gotoCmd.labelTargets.Count()); - var newLabelNames = new List(gotoCmd.labelTargets.Count()); - foreach (var target in gotoCmd.labelTargets) - { - newLabelTargets.Add(oldToNewBlockMap[target]); - newLabelNames.Add(oldToNewBlockMap[target].Label); - } - - oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets); - } - return newBlocks; - } - - private static List PostProcess(List blocks) - { - void DeleteFalseGotos (Block b) - { - bool isAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; } - var firstFalseIdx = b.Cmds.FindIndex(c => isAssumeFalse(c)); - if (firstFalseIdx != -1) - { - b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList(); - b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd; - } - } - - bool ContainsAssert(Block b) - { - bool isNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } - return b.Cmds.Exists(cmd => isNonTrivialAssert(cmd)); - } - - blocks.ForEach(b => DeleteFalseGotos(b)); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously - var todo = new Stack(); - var peeked = new HashSet(); - var interestingBlocks = new HashSet(); - todo.Push(blocks[0]); - while(todo.Count() > 0) - { - var currentBlock = todo.Peek(); - var pop = peeked.Contains(currentBlock); - peeked.Add(currentBlock); - var interesting = false; - var exit = currentBlock.TransferCmd as GotoCmd; - if (exit != null && !pop) { - exit.labelTargets.ForEach(b => todo.Push(b)); - } else if (exit != null) { - Contract.Assert(pop); - var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); - currentBlock.TransferCmd = gtc; - interesting = interesting || gtc.labelTargets.Count() != 0; - } - if (pop) - { - interesting = interesting || ContainsAssert(currentBlock); - if (interesting) { - interestingBlocks.Add(currentBlock); - } - todo.Pop(); - } - } - interestingBlocks.Add(blocks[0]); // must not be empty - return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. - } - - private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here") - || c is AssertCmd && splitOnEveryAssert; - } - - public static List FindManualSplits(Split initialSplit, bool splitOnEveryAssert) - { - Contract.Requires(initialSplit.Implementation != null); - Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); - - var splitPoints = new Dictionary(); - foreach (var b in initialSplit.blocks) - { - foreach (Cmd c in b.Cmds) - { - var p = c as PredicateCmd; - if (ShouldSplitHere(c, splitOnEveryAssert)) - { - splitPoints.TryGetValue(b, out var count); - splitPoints[b] = count + 1; - } - } - } - var splits = new List(); - if (!splitPoints.Any()) - { - splits.Add(initialSplit); - } - else - { - Block entryPoint = initialSplit.blocks[0]; - var blockAssignments = PickBlocksToVerify(initialSplit.blocks, splitPoints); - var entryBlockHasSplit = splitPoints.Keys.Contains(entryPoint); - var baseSplitBlocks = PostProcess(DoPreAssignedManualSplit(initialSplit.options, initialSplit.blocks, blockAssignments, -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert)); - splits.Add(new Split(initialSplit.options, baseSplitBlocks, initialSplit.gotoCmdOrigins, initialSplit.parent, initialSplit.run)); - foreach (KeyValuePair pair in splitPoints) - { - for (int i = 0; i < pair.Value; i++) - { - bool lastSplitInBlock = i == pair.Value - 1; - var newBlocks = DoPreAssignedManualSplit(initialSplit.options, initialSplit.blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert); - splits.Add(new Split(initialSplit.options, PostProcess(newBlocks), initialSplit.gotoCmdOrigins, initialSplit.parent, initialSplit.run)); // REVIEW: Does gotoCmdOrigins need to be changed at all? - } - } - } - return splits; - } - - public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par) - { - bool IsFocusCmd(Cmd c) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); - } - - List GetFocusBlocks(List blocks) { - return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList(); - } - - var impl = run.Implementation; - var dag = Program.GraphFromImpl(impl); - var topoSorted = dag.TopologicalSort().ToList(); - // By default, we process the foci in a top-down fashion, i.e., in the topological order. - // If the user sets the RelaxFocus flag, we use the reverse (topological) order. - var focusBlocks = GetFocusBlocks(topoSorted); - if (par.CheckerPool.Options.RelaxFocus) { - focusBlocks.Reverse(); - } - if (!focusBlocks.Any()) { - var f = new List(); - f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run)); - return f; - } - // finds all the blocks dominated by focusBlock in the subgraph - // which only contains vertices of subgraph. - HashSet DominatedBlocks(Block focusBlock, IEnumerable subgraph) - { - var dominators = new Dictionary>(); - var todo = new Queue(); - foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk))) - { - var s = new HashSet(); - var pred = b.Predecessors.Where(blk => subgraph.Contains(blk)).ToList(); - if (pred.Count != 0) - { - s.UnionWith(dominators[pred[0]]); - pred.ForEach(blk => s.IntersectWith(dominators[blk])); - } - s.Add(b); - dominators[b] = s; - } - return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet(); - } - - Cmd DisableSplits(Cmd c) - { - if (c is PredicateCmd pc) - { - for (var kv = pc.Attributes; kv != null; kv = kv.Next) - { - if (kv.Key == "split") - { - kv.AddParam(new LiteralExpr(Token.NoToken, false)); - } - } - } - return c; - } - - var Ancestors = new Dictionary>(); - var Descendants = new Dictionary>(); - focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet()); - focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet()); - var s = new List(); - var duplicator = new Duplicator(); - void FocusRec(int focusIdx, IEnumerable blocks, IEnumerable freeBlocks) - { - if (focusIdx == focusBlocks.Count()) - { - // it is important for l to be consistent with reverse topological order. - var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse(); - // assert that the root block, impl.Blocks[0], is in l - Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]); - var newBlocks = new List(); - var oldToNewBlockMap = new Dictionary(blocks.Count()); - foreach (Block b in l) - { - var newBlock = (Block)duplicator.Visit(b); - newBlocks.Add(newBlock); - oldToNewBlockMap[b] = newBlock; - // freeBlocks consist of the predecessors of the relevant foci. - // Their assertions turn into assumes and any splits inside them are disabled. - if(freeBlocks.Contains(b)) - { - newBlock.Cmds = b.Cmds.Select(c => Split.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList(); - } - if (b.TransferCmd is GotoCmd gtc) - { - var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk)); - newBlock.TransferCmd = new GotoCmd(gtc.tok, - targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), - targets.Select(blk => oldToNewBlockMap[blk]).ToList()); - } - } - newBlocks.Reverse(); - Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]); - s.Add(new Split(options, PostProcess(newBlocks), gotoCmdOrigins, par, run)); - } - else if (!blocks.Contains(focusBlocks[focusIdx]) - || freeBlocks.Contains(focusBlocks[focusIdx])) - { - FocusRec(focusIdx + 1, blocks, freeBlocks); - } - else - { - var b = focusBlocks[focusIdx]; // assert b in blocks - var dominatedBlocks = DominatedBlocks(b, blocks); - // the first part takes all blocks except the ones dominated by the focus block - FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks); - var ancestors = Ancestors[b]; - ancestors.Remove(b); - var descendants = Descendants[b]; - // the other part takes all the ancestors, the focus block, and the descendants. - FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks)); - } - } - - FocusRec(0, impl.Blocks, new List()); - return s; - } - - public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par, bool splitOnEveryAssert) - { - List focussedImpl = FocusImpl(options, run, gotoCmdOrigins, par); - var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList(); - return splits; - } - public static List /*!*/ DoSplit(Split initial, double splitThreshold, int maxSplits) { Contract.Requires(initial != null); Contract.Ensures(cce.NonNullElements(Contract.Result>())); - var run = initial.run; + var run = initial.Run; var result = new List { initial }; while (result.Count < maxSplits) @@ -1161,7 +798,7 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun Split s0, s1; - bool splitStats = initial.options.TraceVerify; + bool splitStats = initial.Options.TraceVerify; if (splitStats) { @@ -1208,12 +845,12 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun { var ss = new List { - s0.blocks[0], - s1.blocks[0] + s0.Blocks[0], + s1.Blocks[0] }; try { - best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.blocks[0], ss); + best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.Blocks[0], ss); } catch (System.Exception e) { @@ -1234,7 +871,7 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun run.OutputWriter.WriteLine(" --> {0}", s1.Stats); } - if (initial.options.TraceVerify) + if (initial.Options.TraceVerify) { best.Print(); } @@ -1246,60 +883,37 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun return result; } - class BlockListComparer : IEqualityComparer> - { - public bool Equals(List x, List y) - { - return x == y || x.SequenceEqual(y); - } - - public int GetHashCode(List obj) - { - int h = 0; - Contract.Assume(obj != null); - foreach (var b in obj) - { - if (b != null) - { - h += b.GetHashCode(); - } - } - - return h; - } - } - - public (ProverInterface.Outcome outcome, VCResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback) + public (Bpl.Outcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback) { Contract.EnsuresOnThrow(true); - ProverInterface.Outcome outcome = cce.NonNull(checker).ReadOutcome(); + Bpl.Outcome outcome = cce.NonNull(checker).ReadOutcome(); - if (options.Trace && SplitIndex >= 0) + if (Options.Trace && SplitIndex >= 0) { - run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, + Run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, checker.ProverRunTime.TotalSeconds, outcome); } - if (options.Trace && options.TrackVerificationCoverage) { - run.OutputWriter.WriteLine("Proof dependencies:\n {0}", + if (Options.Trace && Options.TrackVerificationCoverage) { + Run.OutputWriter.WriteLine("Proof dependencies:\n {0}", string.Join("\n ", CoveredElements.Select(s => s.Description).OrderBy(s => s))); } var resourceCount = checker.GetProverResourceCount(); - var result = new VCResult( - vcNum: SplitIndex + 1, - iteration: iteration, - startTime: checker.ProverStart, - outcome: outcome, - runTime: checker.ProverRunTime, - maxCounterExamples: checker.Options.ErrorLimit, - counterExamples: Counterexamples, - asserts: Asserts, - coveredElements: CoveredElements, - resourceCount: resourceCount, - solverUsed: (options as SMTLibSolverOptions)?.Solver); + var result = new VerificationRunResult( + VcNum: SplitIndex + 1, + Iteration: iteration, + StartTime: checker.ProverStart, + Outcome: outcome, + RunTime: checker.ProverRunTime, + MaxCounterExamples: checker.Options.ErrorLimit, + CounterExamples: Counterexamples, + Asserts: Asserts, + CoveredElements: CoveredElements, + ResourceCount: resourceCount, + SolverUsed: (Options as SMTLibSolverOptions)?.Solver); callback.OnVCResult(result); - if (options.VcsDumpSplits) + if (Options.VcsDumpSplits) { DumpDot(SplitIndex); } @@ -1323,7 +937,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa VCExpr vc; // Lock impl since we're setting impl.Blocks that is used to generate the VC. lock (Implementation) { - Implementation.Blocks = blocks; + Implementation.Blocks = Blocks; var absyIds = new ControlFlowIdMap(); @@ -1343,13 +957,13 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0])))); vc = exprGen.Implies(eqExpr, vc); - reporter = new VCGen.ErrorReporter(options, gotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, + reporter = new VCGen.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, mvInfo, checker.TheoremProver.Context, parent.program, this); } - if (options.TraceVerify && SplitIndex >= 0) + if (Options.TraceVerify && SplitIndex >= 0) { - run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex); + Run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex); Print(); } @@ -1370,16 +984,6 @@ public string Description } } - private static Cmd AssertIntoAssume(VCGenOptions options, Cmd c) - { - if (c is AssertCmd assrt) - { - return VCGen.AssertTurnedIntoAssume(options, assrt); - } - - return c; - } - private void SoundnessCheck(HashSet /*!*/> /*!*/ cache, Block /*!*/ orig, List /*!*/ copies) { diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index e2e1336a0..d361ada9a 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -7,14 +7,16 @@ using System.Threading; using System.Threading.Tasks; using Microsoft.Boogie; +using VCGeneration; using static VC.ConditionGeneration; +using Outcome = Microsoft.Boogie.Outcome; namespace VC { class SplitAndVerifyWorker { - public IObservable<(Split split, VCResult vcResult)> BatchCompletions => batchCompletions; - private readonly Subject<(Split split, VCResult vcResult)> batchCompletions = new(); + public IObservable<(Split split, VerificationRunResult vcResult)> BatchCompletions => batchCompletions; + private readonly Subject<(Split split, VerificationRunResult vcResult)> batchCompletions = new(); private readonly VCGenOptions options; private readonly VerifierCallback callback; @@ -31,7 +33,7 @@ class SplitAndVerifyWorker private bool KeepGoing => maxKeepGoingSplits > 1; private VCGen vcGen; - private Outcome outcome; + private VcOutcome vcOutcome; private double remainingCost; private double provenCost; private int total; @@ -41,13 +43,13 @@ class SplitAndVerifyWorker public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun run, Dictionary gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, - Outcome outcome) + VcOutcome vcOutcome) { this.options = options; this.callback = callback; this.mvInfo = mvInfo; this.run = run; - this.outcome = outcome; + this.vcOutcome = vcOutcome; this.vcGen = vcGen; var maxSplits = options.VcsMaxSplits; VCGen.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits); @@ -67,7 +69,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); ResetPredecessors(Implementation.Blocks); - manualSplits = Split.FocusAndSplit(options, run, gotoCmdOrigins, vcGen, splitOnEveryAssert); + manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, vcGen, splitOnEveryAssert); if (manualSplits.Count == 1 && maxSplits > 1) { manualSplits = Split.DoSplit(manualSplits[0], maxVcCost, maxSplits); @@ -77,7 +79,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun splitNumber = DoSplitting ? 0 : -1; } - public async Task WorkUntilDone(CancellationToken cancellationToken) + public async Task WorkUntilDone(CancellationToken cancellationToken) { TrackSplitsCost(manualSplits); try @@ -89,7 +91,7 @@ public async Task WorkUntilDone(CancellationToken cancellationToken) batchCompletions.OnCompleted(); } - return outcome; + return vcOutcome; } public int ResourceCount => totalResourceCount; @@ -168,7 +170,7 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch var (newOutcome, result, newResourceCount) = split.ReadOutcome(iteration, checker, callback); lock (this) { - outcome = MergeOutcomes(outcome, newOutcome); + vcOutcome = MergeOutcomes(vcOutcome, newOutcome); totalResourceCount += newResourceCount; } var proverFailed = IsProverFailed(newOutcome); @@ -195,17 +197,17 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch } } - private static bool IsProverFailed(ProverInterface.Outcome outcome) + private static bool IsProverFailed(Outcome outcome) { switch (outcome) { - case ProverInterface.Outcome.Valid: - case ProverInterface.Outcome.Invalid: - case ProverInterface.Outcome.Undetermined: + case Outcome.Valid: + case Outcome.Invalid: + case Outcome.Undetermined: return false; - case ProverInterface.Outcome.OutOfMemory: - case ProverInterface.Outcome.TimeOut: - case ProverInterface.Outcome.OutOfResource: + case Outcome.OutOfMemory: + case Outcome.TimeOut: + case Outcome.OutOfResource: return true; default: Contract.Assert(false); @@ -213,48 +215,48 @@ private static bool IsProverFailed(ProverInterface.Outcome outcome) } } - private static Outcome MergeOutcomes(Outcome currentOutcome, ProverInterface.Outcome newOutcome) + private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, Outcome newOutcome) { switch (newOutcome) { - case ProverInterface.Outcome.Valid: - return currentOutcome; - case ProverInterface.Outcome.Invalid: - return Outcome.Errors; - case ProverInterface.Outcome.OutOfMemory: - if (currentOutcome != Outcome.Errors && currentOutcome != Outcome.Inconclusive) + case Outcome.Valid: + return currentVcOutcome; + case Outcome.Invalid: + return VcOutcome.Errors; + case Outcome.OutOfMemory: + if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) { - return Outcome.OutOfMemory; + return VcOutcome.OutOfMemory; } - return currentOutcome; - case ProverInterface.Outcome.TimeOut: - if (currentOutcome != Outcome.Errors && currentOutcome != Outcome.Inconclusive) + return currentVcOutcome; + case Outcome.TimeOut: + if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) { - return Outcome.TimedOut; + return VcOutcome.TimedOut; } - return currentOutcome; - case ProverInterface.Outcome.OutOfResource: - if (currentOutcome != Outcome.Errors && currentOutcome != Outcome.Inconclusive) + return currentVcOutcome; + case Outcome.OutOfResource: + if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) { - return Outcome.OutOfResource; + return VcOutcome.OutOfResource; } - return currentOutcome; - case ProverInterface.Outcome.Undetermined: - if (currentOutcome != Outcome.Errors) + return currentVcOutcome; + case Outcome.Undetermined: + if (currentVcOutcome != VcOutcome.Errors) { - return Outcome.Inconclusive; + return VcOutcome.Inconclusive; } - return currentOutcome; + return currentVcOutcome; default: Contract.Assert(false); throw new cce.UnreachableException(); } } - private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, VCResult vcResult, CancellationToken cancellationToken) + private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, VerificationRunResult verificationRunResult, CancellationToken cancellationToken) { if (split.LastChance) { string msg = "some timeout"; @@ -266,11 +268,11 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal callback.OnCounterexample(cex, msg); split.Counterexamples.Add(cex); // Update one last time the result with the dummy counter-example to indicate the position of the timeout - var result = vcResult with { - counterExamples = split.Counterexamples + var result = verificationRunResult with { + CounterExamples = split.Counterexamples }; batchCompletions.OnNext((split, result)); - outcome = Outcome.Errors; + vcOutcome = VcOutcome.Errors; await checker.GoBackToIdle(); return; } @@ -286,29 +288,29 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal maxVcCost = 1.0; // for future TrackSplitsCost(newSplits); - if (outcome != Outcome.Errors) { - outcome = Outcome.Correct; + if (vcOutcome != VcOutcome.Errors) { + vcOutcome = VcOutcome.Correct; } await Task.WhenAll(newSplits.Select(newSplit => DoWorkForMultipleIterations(newSplit, cancellationToken))); return; } - Contract.Assert(outcome != Outcome.Correct); - if (outcome == Outcome.TimedOut) { + Contract.Assert(vcOutcome != VcOutcome.Correct); + if (vcOutcome == VcOutcome.TimedOut) { string msg = "some timeout"; if (split.reporter is { resourceExceededMessage: { } }) { msg = split.reporter.resourceExceededMessage; } callback.OnTimeout(msg); - } else if (outcome == Outcome.OutOfMemory) { + } else if (vcOutcome == VcOutcome.OutOfMemory) { string msg = "out of memory"; if (split.reporter is { resourceExceededMessage: { } }) { msg = split.reporter.resourceExceededMessage; } callback.OnOutOfMemory(msg); - } else if (outcome == Outcome.OutOfResource) { + } else if (vcOutcome == VcOutcome.OutOfResource) { string msg = "out of resource"; if (split.reporter is { resourceExceededMessage: { } }) { msg = split.reporter.resourceExceededMessage; @@ -317,7 +319,7 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal callback.OnOutOfResource(msg); } - batchCompletions.OnNext((split, vcResult)); + batchCompletions.OnNext((split, verificationRunResult)); } } } diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index bb48650f4..beb082cb5 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -990,7 +990,7 @@ protected override bool ProcIsLoop(string procname) return true; } - public abstract Outcome FindLeastToVerify(Implementation impl, ref HashSet allBoolVars); + public abstract VcOutcome FindLeastToVerify(Implementation impl, ref HashSet allBoolVars); } } // namespace VC diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index ed3393daa..c0abd717d 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -355,8 +355,8 @@ record ImplementationTransformationData { private static ConditionalWeakTable implementationData = new(); - public override async Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, - CancellationToken cancellationToken, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver) + public override async Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, + CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver) { Contract.EnsuresOnThrow(true); @@ -364,7 +364,7 @@ public override async Task VerifyImplementation(ImplementationRun run, if (run.Implementation.IsSkipVerification(Options)) { - return Outcome.Inconclusive; // not sure about this one + return VcOutcome.Inconclusive; // not sure about this one } callback.OnProgress?.Invoke("VCgen", 0, 0, 0.0); @@ -391,12 +391,12 @@ public override async Task VerifyImplementation(ImplementationRun run, ExpandAsserts(impl); } - Outcome outcome = Outcome.Correct; + VcOutcome vcOutcome = VcOutcome.Correct; // Report all recycled failing assertions for this implementation. if (impl.RecycledFailingAssertions != null && impl.RecycledFailingAssertions.Any()) { - outcome = Outcome.Errors; + vcOutcome = VcOutcome.Errors; foreach (var a in impl.RecycledFailingAssertions) { var checksum = a.Checksum; @@ -417,21 +417,21 @@ public override async Task VerifyImplementation(ImplementationRun run, } var worker = new SplitAndVerifyWorker(Options, this, run, data.GotoCmdOrigins, callback, - data.ModelViewInfo, outcome); + data.ModelViewInfo, vcOutcome); worker.BatchCompletions.Subscribe(batchCompletedObserver); - outcome = await worker.WorkUntilDone(cancellationToken); + vcOutcome = await worker.WorkUntilDone(cancellationToken); ResourceCount = worker.ResourceCount; TotalProverElapsedTime = worker.TotalProverElapsedTime; - if (outcome == Outcome.Correct && smokeTester != null) + if (vcOutcome == VcOutcome.Correct && smokeTester != null) { await smokeTester.Test(run.OutputWriter); } callback.OnProgress?.Invoke("done", 0, 0, 1.0); - return outcome; + return vcOutcome; } public class ErrorReporter : ProverInterface.ErrorHandler { @@ -501,7 +501,7 @@ public ErrorReporter(VCGenOptions options, } public override void OnModel(IList labels /*!*/ /*!*/, Model model, - ProverInterface.Outcome proverOutcome) + Bpl.Outcome proverOutcome) { // no counter examples reported. if (labels.Count == 0) diff --git a/Source/VCGeneration/VerificationResultCollector.cs b/Source/VCGeneration/VerificationResultCollector.cs new file mode 100644 index 000000000..6957914ad --- /dev/null +++ b/Source/VCGeneration/VerificationResultCollector.cs @@ -0,0 +1,45 @@ +using System.Collections.Concurrent; +using System.Diagnostics.Contracts; +using Microsoft.Boogie; + +namespace VC; + +public class VerificationResultCollector : VerifierCallback +{ + private readonly VCGenOptions options; + + public VerificationResultCollector(VCGenOptions options) : base(options.PrintProverWarnings) + { + this.options = options; + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(cce.NonNullElements(examples)); + Contract.Invariant(cce.NonNullElements(vcResults)); + } + + public readonly ConcurrentQueue examples = new(); + public readonly ConcurrentQueue vcResults = new(); + + public override void OnCounterexample(Counterexample ce, string /*?*/ reason) + { + //Contract.Requires(ce != null); + ce.InitializeModelStates(); + examples.Enqueue(ce); + } + + public override void OnUnreachableCode(ImplementationRun run) + { + //Contract.Requires(impl != null); + run.OutputWriter.WriteLine("found unreachable code:"); + ConditionGeneration.EmitImpl(options, run, false); + // TODO report error about next to last in seq + } + + public override void OnVCResult(VerificationRunResult result) + { + vcResults.Enqueue(result); + } +} \ No newline at end of file diff --git a/Source/VCGeneration/VCResult.cs b/Source/VCGeneration/VerificationRunResult.cs similarity index 62% rename from Source/VCGeneration/VCResult.cs rename to Source/VCGeneration/VerificationRunResult.cs index a304b1158..c26e859a5 100644 --- a/Source/VCGeneration/VCResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -15,28 +15,28 @@ namespace VC using Bpl = Microsoft.Boogie; using System.Threading.Tasks; - public record VCResult + public record VerificationRunResult ( - int vcNum, - int iteration, - DateTime startTime, - ProverInterface.Outcome outcome, - TimeSpan runTime, - int maxCounterExamples, - List counterExamples, - List asserts, - IEnumerable coveredElements, - int resourceCount, - SolverKind? solverUsed + int VcNum, + int Iteration, + DateTime StartTime, + Bpl.Outcome Outcome, + TimeSpan RunTime, + int MaxCounterExamples, + List CounterExamples, + List Asserts, + IEnumerable CoveredElements, + int ResourceCount, + SolverKind? SolverUsed ) { - public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, + public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, out Dictionary perAssertCounterExamples) { perAssertOutcome = new(); perAssertCounterExamples = new(); - if (outcome == ProverInterface.Outcome.Valid) { - perAssertOutcome = asserts.ToDictionary(cmd => cmd, assertCmd => ProverInterface.Outcome.Valid); + if (Outcome == Bpl.Outcome.Valid) { + perAssertOutcome = Asserts.ToDictionary(cmd => cmd, assertCmd => Bpl.Outcome.Valid); } else { - foreach (var counterExample in counterExamples) { + foreach (var counterExample in CounterExamples) { AssertCmd underlyingAssert; if (counterExample is AssertCounterexample assertCounterexample) { underlyingAssert = assertCounterexample.FailingAssert; @@ -49,25 +49,25 @@ public void ComputePerAssertOutcomes(out Dictionary