From 5eed5f62056da549028aa3ffb5d7a71698e32606 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 15:07:57 +0200 Subject: [PATCH 01/18] Configure a VC timeout for all tests --- Source/ExecutionEngine/VerificationTask.cs | 5 +++-- Source/VCGeneration/SplitAndVerifyWorker.cs | 2 +- Test/lit.site.cfg | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 297d7619d..75f56f28e 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(); @@ -127,7 +127,8 @@ private async IAsyncEnumerable StartRun([EnumeratorCancella var collector = new VerificationResultCollector(Split.Options); await engine.LargeThreadTaskFactory.StartNew(() => Split.BeginCheck(Split.Run.OutputWriter, checker, collector, - modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken), cancellationToken).Unwrap(); + modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken), cancellationToken).Unwrap(). + WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken); await checker.ProverTask.WaitAsync(cancellationToken); var result = Split.ReadOutcome(0, checker, collector); diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 63b763de0..c5a0333a5 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -150,7 +150,7 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance KeepGoing ? options.VcsKeepGoingTimeout : run.Implementation.GetTimeLimit(options); await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, - Implementation.GetResourceLimit(options), cancellationToken); + Implementation.GetResourceLimit(options), cancellationToken).WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken); } private Implementation Implementation => run.Implementation; diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index fdb6a8681..3c7351a3f 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' # Allow user to provide extra arguments to Boogie boogieParams = lit_config.params.get('boogie_params', '') From c79011bbe26af6ebf7055ef44d0b96901b4f13e3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 15:08:16 +0200 Subject: [PATCH 02/18] Fix concurrency issue in QuantifierInstantiationEngine --- .../VCExpr/QuantifierInstantiationEngine.cs | 40 +++++++++---------- 1 file changed, 19 insertions(+), 21 deletions(-) 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; } From 2870fb01de5ab6a4126cad24e10e52bbed955c3c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 15:20:25 +0200 Subject: [PATCH 03/18] Add a process limit timeout --- Source/BoogieDriver/BoogieDriver.cs | 5 +- Source/ExecutionEngine/CommandLineOptions.cs | 8 ++ Source/ExecutionEngine/ExecutionEngine.cs | 77 +++++-------- .../ExecutionEngineTests/CancellationTests.cs | 109 ------------------ Source/VCGeneration/ConditionGeneration.cs | 2 +- Test/lit.site.cfg | 2 +- Test/prover/cvc5-offline.smt2 | 32 +++++ 7 files changed, 73 insertions(+), 162 deletions(-) delete mode 100644 Source/UnitTests/ExecutionEngineTests/CancellationTests.cs create mode 100644 Test/prover/cvc5-offline.smt2 diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 979806a68..0a1b5955b 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.IO; +using System.Threading; namespace Microsoft.Boogie { @@ -63,8 +64,10 @@ public static int Main(string[] args) Helpers.ExtraTraceInformation(options, "Becoming sentient"); - var success = executionEngine.ProcessFiles(Console.Out, fileList).Result; + var source = new CancellationTokenSource(); + source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit)); + var success = executionEngine.ProcessFiles(Console.Out, fileList, cancellationToken: source.Token).Result; if (options.XmlSink != null) { options.XmlSink.Close(); 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/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index cc37f985a..a1e026246 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -83,20 +83,17 @@ static readonly ConcurrentDictionary static readonly ConcurrentDictionary ImplIdToCancellationTokenSource = new ConcurrentDictionary(); - static readonly ConcurrentDictionary RequestIdToCancellationTokenSource = - new ConcurrentDictionary(); - 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); + success &= await ProcessFiles(output, new List { fileName }, lookForSnapshots, fileName, cancellationToken: cancellationToken); } return success; } @@ -108,7 +105,7 @@ public async Task ProcessFiles(TextWriter output, IList fileNames, // 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; } @@ -120,7 +117,7 @@ public async Task ProcessFiles(TextWriter output, IList fileNames, return true; } - return await ProcessProgram(output, program, bplFileName, programId); + return await ProcessProgram(output, program, bplFileName, programId, cancellationToken: cancellationToken); } [Obsolete("Please inline this method call")] @@ -129,7 +126,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 +144,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 +165,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 +527,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 +540,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 +553,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 +563,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 +577,7 @@ public async Task InferAndVerify( return outcome; } - private Task PreProcessProgramVerification(Program program) + private Task PreProcessProgramVerification(Program program, CancellationToken cancellationToken) { return LargeThreadTaskFactory.StartNew(() => { @@ -613,7 +612,7 @@ private Task PreProcessProgramVerification(Program program) program.DeclarationDependencies = Pruner.ComputeDeclarationDependencies(Options, program); return processedProgram; - }); + }, cancellationToken); } private ProcessedProgram ExtractLoops(Program program) @@ -652,18 +651,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 +678,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 +705,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 +725,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 +787,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 +837,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 +854,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 +887,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 +903,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 +960,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/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/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/Test/lit.site.cfg b/Test/lit.site.cfg index 3c7351a3f..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 -timeLimit:30' +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/prover/cvc5-offline.smt2 b/Test/prover/cvc5-offline.smt2 new file mode 100644 index 000000000..61aaf30b3 --- /dev/null +++ b/Test/prover/cvc5-offline.smt2 @@ -0,0 +1,32 @@ +(set-option :timeout 30000) +(set-option :rlimit 0) +(set-option :smt.mbqi false) +(set-option :model.compact false) +(set-option :model.v2 true) +(set-option :pp.bv_literals false) +(set-option :print-success false) +(set-info :smt-lib-version 2.6) +(set-option :smt.mbqi false) +(set-option :model.compact false) +(set-option :model.v2 true) +(set-option :pp.bv_literals false) +; done setting options + + +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun x () Int) +(declare-fun y () Int) +(push 1) +(set-info :boogie-vc-id P) +(assert (not + (=> (= (ControlFlow 0 0) 3) (let ((anon0_correct (=> (= (ControlFlow 0 2) (- 0 1)) (= (* x y) (* y x))))) +(let ((PreconditionGeneratedEntry_correct (=> (= (ControlFlow 0 3) 2) anon0_correct))) +PreconditionGeneratedEntry_correct))) +)) +(check-sat) +(get-info :reason-unknown) +(get-info :rlimit) +(get-model) +(pop 1) From 735fee450f154912d5f04069a401c9dd603805a5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 15:53:48 +0200 Subject: [PATCH 04/18] Make trace output culture invariant --- Source/Provers/SMTLib/TypeDeclCollector.cs | 16 ++++++++-------- Source/VCGeneration/SplitAndVerifyWorker.cs | 6 ++++-- 2 files changed, 12 insertions(+), 10 deletions(-) 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/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index c5a0333a5..2fbe080a9 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,8 +140,9 @@ 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:0.00}%, {0} ...", - split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost)); + await run.OutputWriter.WriteLineAsync(string.Format(CultureInfo.InvariantCulture, + " checking split {1}/{2}, {3:0.00}%, {0} ...", + split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost))); } callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total, From 830ac55dca8157516b9f834efb88b29b317c5c3c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 16:39:07 +0200 Subject: [PATCH 05/18] Fix Rlimitouts0.bpl --- Source/BoogieDriver/BoogieDriver.cs | 5 ++++- Source/ExecutionEngine/VerificationTask.cs | 10 +++++++--- Source/VCGeneration/SplitAndVerifyWorker.cs | 9 +++++++-- Test/test2/Rlimitouts0.bpl | 2 +- 4 files changed, 19 insertions(+), 7 deletions(-) diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 0a1b5955b..79b86bdd6 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -65,7 +65,10 @@ public static int Main(string[] args) Helpers.ExtraTraceInformation(options, "Becoming sentient"); var source = new CancellationTokenSource(); - source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit)); + if (options.ProcessTimeLimit != 0) + { + source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit)); + } var success = executionEngine.ProcessFiles(Console.Out, fileList, cancellationToken: source.Token).Result; if (options.XmlSink != null) diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 75f56f28e..8ef2793a7 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -126,9 +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, - modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken), cancellationToken).Unwrap(). - WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken); + 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/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 2fbe080a9..fc9ee4287 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -151,8 +151,13 @@ await run.OutputWriter.WriteLineAsync(string.Format(CultureInfo.InvariantCulture var timeout = KeepGoing && split.LastChance ? options.VcsFinalAssertTimeout : KeepGoing ? options.VcsKeepGoingTimeout : run.Implementation.GetTimeLimit(options); - await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, - Implementation.GetResourceLimit(options), cancellationToken).WaitAsync(TimeSpan.FromSeconds(timeout), cancellationToken); + 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/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl index 7a5e011f2..bae6fc5b3 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 -processTimeLimit:0 -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) From 9d5ef3dcd37e24c87f8eafc6e41ce9cc1e52fcbb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 16:45:24 +0200 Subject: [PATCH 06/18] Fix tests --- Test/civl/paxos/is.sh | 2 +- Test/livevars/stack_overflow.bpl | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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/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 From 43ca15e7bf6a5b51ab263d810bdbde147e852ced Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 23:00:25 +0200 Subject: [PATCH 07/18] Fix indentation --- Source/VCGeneration/SplitAndVerifyWorker.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 20a0ba8e7..f06a06edd 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -142,9 +142,9 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}"; 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))); + split.Stats, splitIdxStr, total, + // split is ManualSplit manualSplit ? $" (line {manualSplit.Token.line})" : "", + // 100 * provenCost / (provenCost + remainingCost))); } callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total, From f98fe32ea87614592eacd75e9ae419ed1422bee7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 10:10:00 +0200 Subject: [PATCH 08/18] Fix comp error --- Source/VCGeneration/SplitAndVerifyWorker.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index f06a06edd..37fd641d4 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -143,8 +143,8 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance 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))); + split is ManualSplit manualSplit ? $" (line {manualSplit.Token.line})" : "", + 100 * provenCost / (provenCost + remainingCost))); } callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total, From b57c1ed7ff2001746181a2134aaf8d0d8f422e1d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 11:03:18 +0200 Subject: [PATCH 09/18] Increase timeout of KeyboardClass test --- Test/havoc0/KeyboardClassFindMorePorts.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); From 2b662ef697797004703c0c2480c11293b1cff663 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 12:20:49 +0200 Subject: [PATCH 10/18] Add more cancellation --- Source/BoogieDriver/BoogieDriver.cs | 11 +++++------ Source/ExecutionEngine/ExecutionEngine.cs | 15 ++++++++++++--- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 79b86bdd6..3e69ea093 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -21,6 +21,11 @@ public static int Main(string[] args) { return 1; } + var source = new CancellationTokenSource(); + if (options.ProcessTimeLimit != 0) + { + source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit)); + } using var executionEngine = ExecutionEngine.CreateWithoutSharedCache(options); if (options.ProcessInfoFlags()) @@ -64,12 +69,6 @@ public static int Main(string[] args) Helpers.ExtraTraceInformation(options, "Becoming sentient"); - var source = new CancellationTokenSource(); - if (options.ProcessTimeLimit != 0) - { - source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit)); - } - var success = executionEngine.ProcessFiles(Console.Out, fileList, cancellationToken: source.Token).Result; if (options.XmlSink != null) { diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index a1e026246..4f2529c1f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -93,6 +93,7 @@ public async Task ProcessFiles(TextWriter output, IList fileNames, if (Options.VerifySeparately && 1 < fileNames.Count) { var success = true; foreach (var fileName in fileNames) { + cancellationToken.ThrowIfCancellationRequested(); success &= await ProcessFiles(output, new List { fileName }, lookForSnapshots, fileName, cancellationToken: cancellationToken); } return success; @@ -102,6 +103,7 @@ 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); @@ -110,14 +112,21 @@ public async Task ProcessFiles(TextWriter output, IList fileNames, 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, cancellationToken: cancellationToken); + return ProcessProgram(output, program, bplFileName, programId, cancellationToken: cancellationToken); } [Obsolete("Please inline this method call")] From 1e9f7ce4083dd957408ce5a18f327e8b09bf1201 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 12:43:03 +0200 Subject: [PATCH 11/18] Interrupt threads when disposing custom stack scheduler --- Source/BoogieDriver/BoogieDriver.cs | 10 +++++++++- .../CustomStackSizePoolTaskScheduler.cs | 2 +- Source/ExecutionEngine/ExecutionEngine.cs | 9 +++------ 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 3e69ea093..880620409 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -1,8 +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 { @@ -24,7 +26,8 @@ public static int Main(string[] args) var source = new CancellationTokenSource(); if (options.ProcessTimeLimit != 0) { - source.CancelAfter(TimeSpan.FromSeconds(options.ProcessTimeLimit)); + var span = TimeSpan.FromSeconds(options.ProcessTimeLimit); + source.CancelAfter(span); } using var executionEngine = ExecutionEngine.CreateWithoutSharedCache(options); @@ -81,6 +84,11 @@ public static int Main(string[] args) Console.ReadLine(); } + if (options.ProcessTimeLimit != 0) + { + Console.WriteLine("Finished execution process, cleaning up"); + } + return success ? 0 : 1; } diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs index 78cb49271..68e101a21 100644 --- a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs +++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs @@ -96,7 +96,7 @@ public void Dispose() queue.Clear(); 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 4f2529c1f..d6b2b3a24 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -74,14 +74,11 @@ 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 ImplIdToCancellationTokenSource = new(); private readonly TaskScheduler largeThreadScheduler; private readonly bool disposeScheduler; From 972c9bed4cba010e45cfe04c0e301a5c94b5bc66 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 15:51:50 +0200 Subject: [PATCH 12/18] Add blame-hang-timeout to unit test --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 3d84ae9b0a2456d0fef56940c2ea580d745a6007 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 16:36:45 +0200 Subject: [PATCH 13/18] Fix --- Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs index 68e101a21..ccae135c1 100644 --- a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs +++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs @@ -82,7 +82,8 @@ private void RunItem() var task = queue.Dequeue().Result; TryExecuteTask(task); } catch(Exception e) { - if (e.GetBaseException() is OperationCanceledException) { + if (e is ThreadInterruptedException) { } + else if (e.GetBaseException() is OperationCanceledException) { // Async queue cancels tasks when it is disposed, which happens when this scheduler is disposed } else { throw; From 3e9470bfda78888afc9501281c27e4a8f8f958cb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 16:41:37 +0200 Subject: [PATCH 14/18] Refactoring --- Source/Core/AsyncQueue.cs | 2 +- .../CustomStackSizePoolTaskScheduler.cs | 20 +++++++++++++------ 2 files changed, 15 insertions(+), 7 deletions(-) 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/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs index ccae135c1..1c7772699 100644 --- a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs +++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs @@ -78,14 +78,22 @@ private void WorkLoop() private void RunItem() { - try { + try + { var task = queue.Dequeue().Result; TryExecuteTask(task); - } catch(Exception e) { - if (e is ThreadInterruptedException) { } - else if (e.GetBaseException() is OperationCanceledException) { + } + catch (ThreadInterruptedException e) + { + } + 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; } } @@ -94,7 +102,7 @@ private void RunItem() public void Dispose() { disposeTokenSource.Cancel(); - queue.Clear(); + queue.CancelWaitsAndClear(); foreach (var thread in threads) { thread.Interrupt(); From 2e8ca55a114301b29eab786e97b5ac3a9e80668a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 17:16:00 +0200 Subject: [PATCH 15/18] Fix warning --- Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs index 1c7772699..bec9e1361 100644 --- a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs +++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs @@ -83,7 +83,7 @@ private void RunItem() var task = queue.Dequeue().Result; TryExecuteTask(task); } - catch (ThreadInterruptedException e) + catch (ThreadInterruptedException) { } catch (Exception e) From 02b35616942eb78dae0c9f04eed0684bf63cef6c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 17:28:24 +0200 Subject: [PATCH 16/18] Removed output that causes tests to fail --- Source/BoogieDriver/BoogieDriver.cs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 880620409..0a1ae2fff 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -84,11 +84,6 @@ public static int Main(string[] args) Console.ReadLine(); } - if (options.ProcessTimeLimit != 0) - { - Console.WriteLine("Finished execution process, cleaning up"); - } - return success ? 0 : 1; } From dabf0ef05ae43173d359562e1735a1c9750c5ebd Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sat, 10 Aug 2024 10:18:41 +0200 Subject: [PATCH 17/18] Delete accident --- Test/prover/cvc5-offline.smt2 | 32 -------------------------------- 1 file changed, 32 deletions(-) delete mode 100644 Test/prover/cvc5-offline.smt2 diff --git a/Test/prover/cvc5-offline.smt2 b/Test/prover/cvc5-offline.smt2 deleted file mode 100644 index 61aaf30b3..000000000 --- a/Test/prover/cvc5-offline.smt2 +++ /dev/null @@ -1,32 +0,0 @@ -(set-option :timeout 30000) -(set-option :rlimit 0) -(set-option :smt.mbqi false) -(set-option :model.compact false) -(set-option :model.v2 true) -(set-option :pp.bv_literals false) -(set-option :print-success false) -(set-info :smt-lib-version 2.6) -(set-option :smt.mbqi false) -(set-option :model.compact false) -(set-option :model.v2 true) -(set-option :pp.bv_literals false) -; done setting options - - -(declare-fun tickleBool (Bool) Bool) -(assert (and (tickleBool true) (tickleBool false))) -(declare-fun ControlFlow (Int Int) Int) -(declare-fun x () Int) -(declare-fun y () Int) -(push 1) -(set-info :boogie-vc-id P) -(assert (not - (=> (= (ControlFlow 0 0) 3) (let ((anon0_correct (=> (= (ControlFlow 0 2) (- 0 1)) (= (* x y) (* y x))))) -(let ((PreconditionGeneratedEntry_correct (=> (= (ControlFlow 0 3) 2) anon0_correct))) -PreconditionGeneratedEntry_correct))) -)) -(check-sat) -(get-info :reason-unknown) -(get-info :rlimit) -(get-model) -(pop 1) From 00ef399402f00bcb2499b5f68543ac8ae13509f6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sat, 10 Aug 2024 10:19:05 +0200 Subject: [PATCH 18/18] Add process time limit --- Test/test2/Rlimitouts0.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl index bae6fc5b3..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 -processTimeLimit:0 -timeLimit:0 -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)