From 004e283ce42917fb08b903ec96192b2aacd9a13e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 13 Aug 2024 18:06:16 +0200 Subject: [PATCH] Resolve Boogie test deadlocks (#932) ### Changes - Made a change to the Dispose method of `CustomStackSizePoolTaskScheduler.cs`, so it now interrupts all its thread instead of joining them. I think this was causing the entire Boogie process to hang after it was finished, causing tests to deadlock. - Add `blame-hang-timeout` to the `dotnet test` invocation that runs the NUnit tests, which allows identifying which test fails when the unit tests timeout. - Add an undocumented option `/processTimeLimit` that can be used by tests to let Boogie stop itself after a certain timespan, allowing developers to get a stacktrace of where Boogie was at the point of timeout. - Remove APIs for cancelling requests, which were only available programmatically and not used by Dafny. - Fix a bug that could cause a concurrency related exception in `QuantifierInstantiationInfo`, which was introduced by https://github.com/boogie-org/boogie/pull/862. - Use an invariant culture somewhere in printing debug output, so the Boogie tests locally pass on my machine, despite my European culture. - Some renaming of variations of VerifyImplementation, to make the differences more clear. - Configure a 30 seconds timelimit per VC for all Boogie tests by default. Added an exception for a few slow tests - Let Boogie cancel checking of a VC after its timelimit has passed, regardless of what the solver is doing ### Testing - Did not add any additional tests - Let the test-suite succeed without retries 4 times, in an attempt to determine that it resolves the test instabilities we've had. --- .github/workflows/test.yml | 2 +- Source/BoogieDriver/BoogieDriver.cs | 12 +- Source/Core/AsyncQueue.cs | 2 +- Source/ExecutionEngine/CommandLineOptions.cs | 8 ++ .../CustomStackSizePoolTaskScheduler.cs | 21 +++- Source/ExecutionEngine/ExecutionEngine.cs | 99 +++++++--------- Source/ExecutionEngine/VerificationTask.cs | 9 +- Source/Provers/SMTLib/TypeDeclCollector.cs | 16 +-- .../ExecutionEngineTests/CancellationTests.cs | 109 ------------------ .../VCExpr/QuantifierInstantiationEngine.cs | 40 +++---- Source/VCGeneration/ConditionGeneration.cs | 2 +- Source/VCGeneration/SplitAndVerifyWorker.cs | 17 ++- Test/civl/paxos/is.sh | 2 +- Test/havoc0/KeyboardClassFindMorePorts.bpl | 2 +- Test/lit.site.cfg | 2 +- Test/livevars/stack_overflow.bpl | 2 +- Test/test2/Rlimitouts0.bpl | 2 +- 17 files changed, 128 insertions(+), 219 deletions(-) delete mode 100644 Source/UnitTests/ExecutionEngineTests/CancellationTests.cs diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index bd4da57ee..a6dd22691 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -60,7 +60,7 @@ jobs: # Create packages dotnet pack --no-build -c ${{ matrix.configuration }} ${SOLUTION} # Run unit tests - dotnet test --no-build -c ${{ matrix.configuration }} ${SOLUTION} + dotnet test --blame-hang-timeout 120s --no-build -c ${{ matrix.configuration }} ${SOLUTION} # Run lit test suite lit --param ${{ matrix.lit_param }} -v --timeout=120 -D configuration=${{ matrix.configuration }} Test - name: Deploy to nuget diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 979806a68..0a1ae2fff 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -1,7 +1,10 @@ using System; using System.Collections.Generic; +using System.Diagnostics; using System.Diagnostics.Contracts; using System.IO; +using System.Threading; +using System.Threading.Tasks; namespace Microsoft.Boogie { @@ -20,6 +23,12 @@ public static int Main(string[] args) { return 1; } + var source = new CancellationTokenSource(); + if (options.ProcessTimeLimit != 0) + { + var span = TimeSpan.FromSeconds(options.ProcessTimeLimit); + source.CancelAfter(span); + } using var executionEngine = ExecutionEngine.CreateWithoutSharedCache(options); if (options.ProcessInfoFlags()) @@ -63,8 +72,7 @@ public static int Main(string[] args) Helpers.ExtraTraceInformation(options, "Becoming sentient"); - var success = executionEngine.ProcessFiles(Console.Out, fileList).Result; - + var success = executionEngine.ProcessFiles(Console.Out, fileList, cancellationToken: source.Token).Result; if (options.XmlSink != null) { options.XmlSink.Close(); diff --git a/Source/Core/AsyncQueue.cs b/Source/Core/AsyncQueue.cs index f20234e80..b051003c8 100644 --- a/Source/Core/AsyncQueue.cs +++ b/Source/Core/AsyncQueue.cs @@ -47,7 +47,7 @@ public IEnumerable Items } } - public void Clear() { + public void CancelWaitsAndClear() { while (customers.TryDequeue(out var customer)) { customer.TrySetCanceled(); } diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 426c46e0b..ec04e7144 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -479,6 +479,10 @@ public int BracketIdsInVC } } + /// + /// A hidden option that configures a time limit for the whole Boogie CLI invocation + /// + public uint ProcessTimeLimit { get; set; } = 0; public uint TimeLimit { get; set; } = 0; // 0 means no limit public uint ResourceLimit { get; set; } = 0; // default to 0 public uint SmokeTimeout { get; set; } = 10; // default to 10s @@ -1273,6 +1277,10 @@ protected override bool ParseOption(string name, CommandLineParseState ps) case "timeLimit": ps.GetUnsignedNumericArgument(x => TimeLimit = x, null); return true; + + case "processTimeLimit": + ps.GetUnsignedNumericArgument(x => ProcessTimeLimit = x, null); + return true; case "rlimit": ps.GetUnsignedNumericArgument(x => ResourceLimit = x); diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs index 78cb49271..bec9e1361 100644 --- a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs +++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs @@ -78,13 +78,22 @@ private void WorkLoop() private void RunItem() { - try { + try + { var task = queue.Dequeue().Result; TryExecuteTask(task); - } catch(Exception e) { - if (e.GetBaseException() is OperationCanceledException) { + } + catch (ThreadInterruptedException) + { + } + catch (Exception e) + { + if (e.GetBaseException() is OperationCanceledException) + { // Async queue cancels tasks when it is disposed, which happens when this scheduler is disposed - } else { + } + else + { throw; } } @@ -93,10 +102,10 @@ private void RunItem() public void Dispose() { disposeTokenSource.Cancel(); - queue.Clear(); + queue.CancelWaitsAndClear(); foreach (var thread in threads) { - thread.Join(); + thread.Interrupt(); } } } \ No newline at end of file diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index cc37f985a..d6b2b3a24 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -74,29 +74,24 @@ public static ExecutionEngine CreateWithoutSharedCache(ExecutionEngineOptions op static DateTime FirstRequestStart; - static readonly ConcurrentDictionary - TimePerRequest = new ConcurrentDictionary(); + static readonly ConcurrentDictionary TimePerRequest = new(); - static readonly ConcurrentDictionary StatisticsPerRequest = - new ConcurrentDictionary(); + static readonly ConcurrentDictionary StatisticsPerRequest = new(); - static readonly ConcurrentDictionary ImplIdToCancellationTokenSource = - new ConcurrentDictionary(); - - static readonly ConcurrentDictionary RequestIdToCancellationTokenSource = - new ConcurrentDictionary(); + static readonly ConcurrentDictionary ImplIdToCancellationTokenSource = new(); private readonly TaskScheduler largeThreadScheduler; private readonly bool disposeScheduler; public async Task ProcessFiles(TextWriter output, IList fileNames, bool lookForSnapshots = true, - string programId = null) { + string programId = null, CancellationToken cancellationToken = default) { Contract.Requires(cce.NonNullElements(fileNames)); if (Options.VerifySeparately && 1 < fileNames.Count) { var success = true; foreach (var fileName in fileNames) { - success &= await ProcessFiles(output, new List { fileName }, lookForSnapshots, fileName); + cancellationToken.ThrowIfCancellationRequested(); + success &= await ProcessFiles(output, new List { fileName }, lookForSnapshots, fileName, cancellationToken: cancellationToken); } return success; } @@ -105,22 +100,30 @@ public async Task ProcessFiles(TextWriter output, IList fileNames, var snapshotsByVersion = LookForSnapshots(fileNames); var success = true; foreach (var snapshots in snapshotsByVersion) { + cancellationToken.ThrowIfCancellationRequested(); // BUG: Reusing checkers during snapshots doesn't work, even though it should. We create a new engine (and thus checker pool) to workaround this. using var engine = new ExecutionEngine(Options, Cache, CustomStackSizePoolTaskScheduler.Create(StackSize, Options.VcsCores), true); - success &= await engine.ProcessFiles(output, new List(snapshots), false, programId); + success &= await engine.ProcessFiles(output, new List(snapshots), false, programId, cancellationToken: cancellationToken); } return success; } + return await ProcessProgramFiles(output, fileNames, programId, cancellationToken); + } + + private Task ProcessProgramFiles(TextWriter output, IList fileNames, string programId, + CancellationToken cancellationToken) + { using XmlFileScope xf = new XmlFileScope(Options.XmlSink, fileNames[^1]); Program program = ParseBoogieProgram(fileNames, false); var bplFileName = fileNames[^1]; - if (program == null) { - return true; + if (program == null) + { + return Task.FromResult(true); } - return await ProcessProgram(output, program, bplFileName, programId); + return ProcessProgram(output, program, bplFileName, programId, cancellationToken: cancellationToken); } [Obsolete("Please inline this method call")] @@ -129,7 +132,7 @@ public bool ProcessProgram(Program program, string bplFileName, return ProcessProgram(Options.OutputWriter, program, bplFileName, programId).Result; } - public async Task ProcessProgram(TextWriter output, Program program, string bplFileName, string programId = null) + public async Task ProcessProgram(TextWriter output, Program program, string bplFileName, string programId = null, CancellationToken cancellationToken = default) { if (programId == null) { @@ -147,7 +150,7 @@ public async Task ProcessProgram(TextWriter output, Program program, strin if (Options.PrintCFGPrefix != null) { foreach (var impl in program.Implementations) { - using StreamWriter sw = new StreamWriter(Options.PrintCFGPrefix + "." + impl.Name + ".dot"); + await using StreamWriter sw = new StreamWriter(Options.PrintCFGPrefix + "." + impl.Name + ".dot"); await sw.WriteAsync(program.ProcessLoops(Options, impl).ToDot()); } } @@ -168,7 +171,7 @@ public async Task ProcessProgram(TextWriter output, Program program, strin Inline(program); var stats = new PipelineStatistics(); - outcome = await InferAndVerify(output, program, stats, 1 < Options.VerifySnapshots ? programId : null); + outcome = await InferAndVerify(output, program, stats, 1 < Options.VerifySnapshots ? programId : null, cancellationToken: cancellationToken); switch (outcome) { case PipelineOutcome.Done: case PipelineOutcome.VerificationCompleted: @@ -530,7 +533,8 @@ public async Task InferAndVerify( Program program, PipelineStatistics stats, string programId = null, - ErrorReporterDelegate er = null, string requestId = null) + ErrorReporterDelegate er = null, string requestId = null, + CancellationToken cancellationToken = default) { Contract.Requires(program != null); Contract.Requires(stats != null); @@ -542,7 +546,7 @@ public async Task InferAndVerify( var start = DateTime.UtcNow; - var processedProgram = await PreProcessProgramVerification(program); + var processedProgram = await PreProcessProgramVerification(program, cancellationToken); foreach (var action in Options.UseResolvedProgram) { action(Options, processedProgram); @@ -555,7 +559,7 @@ public async Task InferAndVerify( if (Options.ContractInfer) { - return await RunHoudini(program, stats, er); + return await RunHoudini(program, stats, er, cancellationToken); } var stablePrioritizedImpls = GetPrioritizedImplementations(program); @@ -565,7 +569,8 @@ public async Task InferAndVerify( out stats.CachingActionCounts); } - var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls); + var outcome = await VerifyEachImplementation(output, processedProgram, stats, + programId, er, stablePrioritizedImpls, cancellationToken); if (1 < Options.VerifySnapshots && programId != null) { @@ -578,7 +583,7 @@ public async Task InferAndVerify( return outcome; } - private Task PreProcessProgramVerification(Program program) + private Task PreProcessProgramVerification(Program program, CancellationToken cancellationToken) { return LargeThreadTaskFactory.StartNew(() => { @@ -613,7 +618,7 @@ private Task PreProcessProgramVerification(Program program) program.DeclarationDependencies = Pruner.ComputeDeclarationDependencies(Options, program); return processedProgram; - }); + }, cancellationToken); } private ProcessedProgram ExtractLoops(Program program) @@ -652,18 +657,16 @@ private Implementation[] GetPrioritizedImplementations(Program program) private async Task VerifyEachImplementation(TextWriter outputWriter, ProcessedProgram processedProgram, PipelineStatistics stats, - string programId, ErrorReporterDelegate er, string requestId, Implementation[] stablePrioritizedImpls) + string programId, ErrorReporterDelegate er, Implementation[] stablePrioritizedImpls, + CancellationToken cancellationToken) { var consoleCollector = new ConcurrentToSequentialWriteManager(outputWriter); - - var cts = new CancellationTokenSource(); - RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts); var tasks = stablePrioritizedImpls.Select(async (impl, index) => { await using var taskWriter = consoleCollector.AppendWriter(); var implementation = stablePrioritizedImpls[index]; var result = await EnqueueVerifyImplementation(processedProgram, stats, programId, er, - implementation, cts, taskWriter); + implementation, cancellationToken, taskWriter); var output = result.GetOutput(Options.Printer, this, stats, er); await taskWriter.WriteAsync(output); return result; @@ -681,9 +684,6 @@ private async Task VerifyEachImplementation(TextWriter outputWr Options.Printer.ErrorWriteLine(outputWriter, "Fatal Error: ProverException: {0}", e.Message); outcome = PipelineOutcome.FatalError; } - finally { - CleanupRequest(requestId); - } if (Options.Trace && Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { Options.OutputWriter.WriteLine("Proof dependencies of whole program:\n {0}", @@ -711,7 +711,7 @@ public void Error(IToken tok, string msg) } } - public async Task> GetVerificationTasks(Program program) + public async Task> GetVerificationTasks(Program program, CancellationToken cancellationToken = default) { var sink = new CollectingErrorSink(); var resolutionErrors = program.Resolve(Options, sink); @@ -731,7 +731,7 @@ public async Task> GetVerificationTasks(Program CoalesceBlocks(program); Inline(program); - var processedProgram = await PreProcessProgramVerification(program); + var processedProgram = await PreProcessProgramVerification(program, cancellationToken); return GetPrioritizedImplementations(program).SelectMany(implementation => { var writer = TextWriter.Null; @@ -793,7 +793,7 @@ private async Task EnqueueVerifyImplementation( await verifyImplementationSemaphore.WaitAsync(cancellationToken); try { - return await VerifyImplementation(processedProgram, stats, errorReporterDelegate, + return await VerifyImplementationWithCaching(processedProgram, stats, errorReporterDelegate, cancellationToken, implementation, programId, taskWriter); } finally @@ -843,25 +843,7 @@ private void TraceCachingForBenchmarking(PipelineStatistics stats, } } - public static void CancelRequest(string requestId) - { - Contract.Requires(requestId != null); - - if (RequestIdToCancellationTokenSource.TryGetValue(requestId, out var cts)) - { - cts.Cancel(); - } - } - - private static void CleanupRequest(string requestId) - { - if (requestId != null) - { - RequestIdToCancellationTokenSource.TryRemove(requestId, out var old); - } - } - - private async Task VerifyImplementation( + private async Task VerifyImplementationWithCaching( ProcessedProgram processedProgram, PipelineStatistics stats, ErrorReporterDelegate er, @@ -878,7 +860,7 @@ private async Task VerifyImplementation( Options.Printer.Inform("", traceWriter); // newline Options.Printer.Inform($"Verifying {implementation.VerboseName} ...", traceWriter); - var result = await VerifyImplementationWithoutCaching(processedProgram, stats, er, cancellationToken, + var result = await VerifyImplementationWithLargeThread(processedProgram, stats, er, cancellationToken, programId, implementation, traceWriter); if (0 < Options.VerifySnapshots && !string.IsNullOrEmpty(implementation.Checksum)) { @@ -911,7 +893,7 @@ public ImplementationRunResult GetCachedVerificationResult(Implementation impl, return null; } - private Task VerifyImplementationWithoutCaching(ProcessedProgram processedProgram, + private Task VerifyImplementationWithLargeThread(ProcessedProgram processedProgram, PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken, string programId, Implementation impl, TextWriter traceWriter) { @@ -927,7 +909,7 @@ private Task VerifyImplementationWithoutCaching(Process try { (verificationResult.VcOutcome, verificationResult.Errors, verificationResult.RunResults) = - await vcGen.VerifyImplementation2(new ImplementationRun(impl, traceWriter), cancellationToken); + await vcGen.VerifyImplementationDirectly(new ImplementationRun(impl, traceWriter), cancellationToken); processedProgram.PostProcessResult(vcGen, impl, verificationResult); } catch (VCGenException e) @@ -984,7 +966,8 @@ private Task VerifyImplementationWithoutCaching(Process #region Houdini - private async Task RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er) + private async Task RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er, + CancellationToken cancellationToken) { Contract.Requires(stats != null); diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 297d7619d..8ef2793a7 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -115,7 +115,7 @@ public void Cancel() { private async IAsyncEnumerable StartRun([EnumeratorCancellation] CancellationToken cancellationToken) { var timeout = Split.Run.Implementation.GetTimeLimit(Split.Options); - + var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, CancellationToken.None); if (!checkerTask.IsCompleted) { yield return new Queued(); @@ -126,8 +126,13 @@ private async IAsyncEnumerable StartRun([EnumeratorCancella yield return new Running(); var collector = new VerificationResultCollector(Split.Options); - await engine.LargeThreadTaskFactory.StartNew(() => Split.BeginCheck(Split.Run.OutputWriter, checker, collector, + var beginCheckTask = engine.LargeThreadTaskFactory.StartNew(() => Split.BeginCheck(Split.Run.OutputWriter, checker, collector, modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken), cancellationToken).Unwrap(); + if (timeout != 0) + { + beginCheckTask = beginCheckTask.WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken); + } + await beginCheckTask; await checker.ProverTask.WaitAsync(cancellationToken); var result = Split.ReadOutcome(0, checker, collector); diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 6f034db03..dac076b12 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -15,7 +15,7 @@ public class TypeDeclCollector : BoundVarTraversingVCExprVisitor private UniqueNamer Namer; private HashSet /*!*/ - RegisteredRelations = new HashSet(); + RegisteredRelations = new(); [ContractInvariantMethod] void ObjectInvariant() @@ -43,8 +43,8 @@ protected override bool StandardResult(VCExpr node, bool arg) return true; } - private readonly List!*/> AllDecls = new List(); - private readonly List!*/> IncDecls = new List(); + private readonly List!*/> AllDecls = new(); + private readonly List!*/> IncDecls = new(); // In order to support push/pop interface of the theorem prover, the "known" declarations // must be kept in a stack @@ -75,12 +75,12 @@ private HashSet /*!*/ KnownSelectFunctions } // ------ - private readonly Stack /*!*/> _KnownFunctions = new Stack>(); - private readonly Stack /*!*/> _KnownVariables = new Stack>(); + private readonly Stack /*!*/> _KnownFunctions = new(); + private readonly Stack /*!*/> _KnownVariables = new(); - private readonly Stack /*!*/> _KnownTypes = new Stack>(); - private readonly Stack /*!*/> _KnownStoreFunctions = new Stack>(); - private readonly Stack /*!*/> _KnownSelectFunctions = new Stack>(); + private readonly Stack /*!*/> _KnownTypes = new(); + private readonly Stack /*!*/> _KnownStoreFunctions = new(); + private readonly Stack /*!*/> _KnownSelectFunctions = new(); private void InitializeKnownDecls() { diff --git a/Source/UnitTests/ExecutionEngineTests/CancellationTests.cs b/Source/UnitTests/ExecutionEngineTests/CancellationTests.cs deleted file mode 100644 index dee86df4c..000000000 --- a/Source/UnitTests/ExecutionEngineTests/CancellationTests.cs +++ /dev/null @@ -1,109 +0,0 @@ -using System; -using System.IO; -using System.Threading.Tasks; -using Microsoft.Boogie; -using NUnit.Framework; - -namespace ExecutionEngineTests -{ - [TestFixture] - public class CancellationTests - { - public Program GetProgram(ExecutionEngine engine, string code) { - var bplFileName = "1"; - int errorCount = Parser.Parse(code, bplFileName, out Program program, - engine.Options.UseBaseNameForFileName); - Assert.AreEqual(0, errorCount); - - engine.ResolveAndTypecheck(program, bplFileName, out _); - engine.EliminateDeadVariables(program); - engine.CollectModSets(program); - engine.CoalesceBlocks(program); - engine.Inline(program); - return program; - } - - [Test] - public async Task InferAndVerifyCanBeCancelledWhileWaitingForProver() { - var options = CommandLineOptions.FromArguments(TextWriter.Null); - using var executionEngine = ExecutionEngine.CreateWithoutSharedCache(options); - var infiniteProgram = GetProgram(executionEngine, SuperSlow); - var terminatingProgram = GetProgram(executionEngine, Fast); - - // We limit the number of checkers to 1. - options.VcsCores = 1; - - var requestId = ExecutionEngine.FreshRequestId(); - var outcomeTask = - executionEngine.InferAndVerify(Console.Out, infiniteProgram, new PipelineStatistics(), requestId, null, requestId); - await Task.Delay(1000); - ExecutionEngine.CancelRequest(requestId); - var outcome = await outcomeTask; - Assert.AreEqual(PipelineOutcome.Cancelled, outcome); - var requestId2 = ExecutionEngine.FreshRequestId(); - var outcome2 = await executionEngine.InferAndVerify(Console.Out, terminatingProgram, new PipelineStatistics(), requestId2, null, requestId2); - Assert.AreEqual(PipelineOutcome.VerificationCompleted, outcome2); - } - - private const string Fast = @" -procedure easy() ensures 1 + 1 == 0; { -} -"; - - private const string SuperSlow = @" - type LayerType; - function {:identity} LitInt(x: int) : int; - axiom (forall x: int :: {:identity} { LitInt(x): int } LitInt(x): int == x); - const $LZ: LayerType; - function $LS(LayerType) : LayerType; - - function Ack($ly: LayerType, m#0: int, n#0: int) : int; - function Ack#canCall(m#0: int, n#0: int) : bool; - axiom (forall $ly: LayerType, m#0: int, n#0: int :: - { Ack($LS($ly), m#0, n#0) } - Ack($LS($ly), m#0, n#0) - == Ack($ly, m#0, n#0)); - axiom (forall $ly: LayerType, m#0: int, n#0: int :: - { Ack($LS($ly), m#0, n#0) } - Ack#canCall(m#0, n#0) - || (m#0 >= LitInt(0) && n#0 >= LitInt(0)) - ==> (m#0 != LitInt(0) - ==> (n#0 == LitInt(0) ==> Ack#canCall(m#0 - 1, LitInt(1))) - && (n#0 != LitInt(0) - ==> Ack#canCall(m#0, n#0 - 1) - && Ack#canCall(m#0 - 1, Ack($ly, m#0, n#0 - 1)))) - && Ack($LS($ly), m#0, n#0) - == (if m#0 == LitInt(0) - then n#0 + 1 - else (if n#0 == LitInt(0) - then Ack($ly, m#0 - 1, LitInt(1)) - else Ack($ly, m#0 - 1, Ack($ly, m#0, n#0 - 1))))); - axiom (forall $ly: LayerType, m#0: int, n#0: int :: - {:weight 3} { Ack($LS($ly), LitInt(m#0), LitInt(n#0)) } - Ack#canCall(LitInt(m#0), LitInt(n#0)) - || (LitInt(m#0) >= LitInt(0) - && LitInt(n#0) >= LitInt(0)) - ==> (LitInt(m#0) != LitInt(0) - ==> (LitInt(n#0) == LitInt(0) - ==> Ack#canCall(LitInt(m#0 - 1), LitInt(1))) - && (LitInt(n#0) != LitInt(0) - ==> Ack#canCall(LitInt(m#0), LitInt(n#0 - 1)) - && Ack#canCall(LitInt(m#0 - 1), - LitInt(Ack($LS($ly), LitInt(m#0), LitInt(n#0 - 1)))))) - && Ack($LS($ly), LitInt(m#0), LitInt(n#0)) - == (if LitInt(m#0) == LitInt(0) - then n#0 + 1 - else (if LitInt(n#0) == LitInt(0) - then Ack($LS($ly), LitInt(m#0 - 1), LitInt(1)) - else Ack($LS($ly), - LitInt(m#0 - 1), - LitInt(Ack($LS($ly), LitInt(m#0), LitInt(n#0 - 1))))))); - - procedure proof() - { - assume Ack#canCall(LitInt(5), LitInt(5)); - assert LitInt(Ack($LS($LS($LZ)), LitInt(5), LitInt(5))) == LitInt(0); - } -"; - } -} \ No newline at end of file diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs index fbb26a262..82991c1b4 100644 --- a/Source/VCExpr/QuantifierInstantiationEngine.cs +++ b/Source/VCExpr/QuantifierInstantiationEngine.cs @@ -51,7 +51,7 @@ public QuantifierInstantiationInfo(Dictionary> boundV private string skolemConstantNamePrefix; internal VCExpressionGenerator vcExprGen; private Boogie2VCExprTranslator exprTranslator; - internal static ConcurrentDictionary> labelToTypes = new(); // pool name may map to multiple types + internal static ConcurrentDictionary> labelToTypes = new(); // pool name may map to multiple types public static VCExpr Instantiate(Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr) { @@ -162,30 +162,28 @@ public void AddLambdaInstances(Dictionary>> lambd public static HashSet FindInstantiationHints(Variable v) { var labels = new HashSet(); - var iter = v.Attributes; - while (iter != null) + for(var iter = v.Attributes; iter != null; iter = iter.Next) { - if (iter.Key == "pool") + if (iter.Key != "pool") + { + continue; + } + + var tok = iter.tok; + foreach(var x in iter.Params) { - var tok = iter.tok; - iter.Params.ForEach(x => + if (x is string poolName) { - if (x is string poolName) - { - labels.Add(poolName); - if (!labelToTypes.ContainsKey(poolName)) - { - labelToTypes[poolName] = new(); - } - labelToTypes[poolName].Add(v.TypedIdent.Type); - } - else - { - Console.WriteLine($"{tok.filename}({tok.line},{tok.col}): expected pool name"); - } - }); + labels.Add(poolName); + var types = labelToTypes.GetOrAdd(poolName, _ => new()); + + types.Add(v.TypedIdent.Type); + } + else + { + Console.WriteLine($"{tok.filename}({tok.line},{tok.col}): expected pool name"); + } } - iter = iter.Next; } return labels; } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index f0f481b8e..44eec8d9b 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -105,7 +105,7 @@ public ConditionGeneration(Program program, CheckerPool checkerPool) /// /// /// - public async Task<(VcOutcome, List errors, List vcResults)> VerifyImplementation2( + public async Task<(VcOutcome, List errors, List vcResults)> VerifyImplementationDirectly( ImplementationRun run, CancellationToken cancellationToken) { Contract.Requires(run != null); diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index a4112ccf2..37fd641d4 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Globalization; using System.Linq; using System.Threading; using System.Threading.Tasks; @@ -139,10 +140,11 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance { var splitNum = split.SplitIndex + 1; var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}"; - run.OutputWriter.WriteLine(" checking split {1}/{2}{3}, {4:0.00}%, {0} ...", - split.Stats, splitIdxStr, total, - split is ManualSplit manualSplit ? $" (line {manualSplit.Token.line})" : "", - 100 * provenCost / (provenCost + remainingCost)); + await run.OutputWriter.WriteLineAsync(string.Format(CultureInfo.InvariantCulture, + " checking split {1}/{2}{3}, {4:0.00}%, {0} ...", + split.Stats, splitIdxStr, total, + split is ManualSplit manualSplit ? $" (line {manualSplit.Token.line})" : "", + 100 * provenCost / (provenCost + remainingCost))); } callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total, @@ -151,8 +153,13 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance var timeout = KeepGoing && split.LastChance ? options.VcsFinalAssertTimeout : KeepGoing ? options.VcsKeepGoingTimeout : run.Implementation.GetTimeLimit(options); - await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, + var beginCheckTask = split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, Implementation.GetResourceLimit(options), cancellationToken); + if (timeout != 0) + { + beginCheckTask = beginCheckTask.WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken); + } + await beginCheckTask; } private Implementation Implementation => run.Implementation; diff --git a/Test/civl/paxos/is.sh b/Test/civl/paxos/is.sh index bc50a3345..cfa524668 100755 --- a/Test/civl/paxos/is.sh +++ b/Test/civl/paxos/is.sh @@ -1,6 +1,6 @@ #!/bin/bash -# RUN: %parallel-boogie Paxos.bpl PaxosActions.bpl PaxosImpl.bpl PaxosSeq.bpl > "%t" +# RUN: %parallel-boogie Paxos.bpl PaxosActions.bpl PaxosImpl.bpl PaxosSeq.bpl /timeLimit:120 > "%t" # RUN: %diff "%s.expect" "%t" boogie $@ Paxos.bpl PaxosActions.bpl PaxosImpl.bpl PaxosSeq.bpl diff --git a/Test/havoc0/KeyboardClassFindMorePorts.bpl b/Test/havoc0/KeyboardClassFindMorePorts.bpl index a5ed4e785..31577360f 100644 --- a/Test/havoc0/KeyboardClassFindMorePorts.bpl +++ b/Test/havoc0/KeyboardClassFindMorePorts.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie "%s" > "%t" +// RUN: %parallel-boogie "%s" /timeLimit:90 > "%t" // RUN: %diff success.expect "%t" type byte, name; function OneByteToInt(byte) returns (int); diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index fdb6a8681..8ea897da8 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -93,7 +93,7 @@ if runtime and lit.util.which(runtime) == None: boogieExecutable = runtime + ' ' + quotePath(boogieExecutable) # We do not want absolute or relative paths in error messages, just the basename of the file -boogieExecutable += ' -useBaseNameForFileName' +boogieExecutable += ' -useBaseNameForFileName -timeLimit:30 -processTimeLimit:110' # Allow user to provide extra arguments to Boogie boogieParams = lit_config.params.get('boogie_params', '') diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl index ca509a99d..a9103e0a3 100644 --- a/Test/livevars/stack_overflow.bpl +++ b/Test/livevars/stack_overflow.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /errorTrace:0 "%s" > "%t" +// RUN: %parallel-boogie /errorTrace:0 /timeLimit:120 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Stress test that we really don't need ot run multiple times diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl index 7a5e011f2..db3fc72bc 100644 --- a/Test/test2/Rlimitouts0.bpl +++ b/Test/test2/Rlimitouts0.bpl @@ -1,5 +1,5 @@ // We use boogie here because parallel-boogie doesn't work well with -proverLog -// RUN: %boogie -rlimit:800000 -proverLog:"%t.smt2" "%s" +// RUN: %boogie -timeLimit:0 -rlimit:800000 -proverLog:"%t.smt2" "%s" // RUN: %OutputCheck --file-to-check "%t.smt2" "%s" // CHECK-L: (set-option :timeout 4000) // CHECK-L: (set-option :rlimit 800000)