From a11f4f1069ca918fb17aeed6673c719dc477debf Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 20 Nov 2023 15:49:25 +0100 Subject: [PATCH 1/4] Update version, and remove race condition --- Source/Directory.Build.props | 2 +- Source/Provers/SMTLib/ProverInterface.cs | 10 ++---- .../SMTLib/SMTLibProcessTheoremProver.cs | 33 +++++++++---------- Source/Provers/SMTLib/SMTLibSolverOptions.cs | 6 ++-- Source/VCGeneration/Split.cs | 4 +-- Source/VCGeneration/SplitAndVerifyWorker.cs | 2 -- 6 files changed, 22 insertions(+), 35 deletions(-) diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index 90edb5ff6..4304646ba 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.0.6 + 3.0.7 net6.0 false Boogie diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index c5da1ff8a..88fedd871 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -270,16 +270,10 @@ public virtual void SetRlimit(uint limit) { } - // Sets a local SMT option (cleared with ClearLocalSMTOptions) - public virtual void SetLocalSMTOption(string name, string value) + public virtual void SetAdditionalSmtOptions(IEnumerable entries) { } - - // Clear options set with SetLocalSMTOption - public virtual void ClearLocalSMTOptions() - { - } - + public virtual Task GetRCount() { throw new NotImplementedException(); diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs index 9c8040712..5490c52db 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -19,6 +19,7 @@ public abstract class SMTLibProcessTheoremProver : ProverInterface protected SMTLibProverContext ctx; protected VCExpressionGenerator gen; protected SMTLibSolverOptions options; + protected IEnumerable additionalSmtOptions = Array.Empty(); protected bool usingUnsatCore; private string backgroundPredicates; @@ -46,7 +47,7 @@ private void ObjectInvariant() } [NotDelayed] - public SMTLibProcessTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions options, VCExpressionGenerator gen, + protected SMTLibProcessTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions options, VCExpressionGenerator gen, SMTLibProverContext ctx) { Contract.Requires(options != null); @@ -346,10 +347,7 @@ protected virtual void PrepareCommon() SendCommon("(set-option :produce-models true)"); } - foreach (var opt in options.SmtOptions) - { - SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); - } + SendSolverOptions(); if (!string.IsNullOrEmpty(options.Logic)) { @@ -393,6 +391,14 @@ protected virtual void PrepareCommon() } } + private void SendSolverOptions() + { + foreach (var opt in options.SmtOptions.Concat(additionalSmtOptions)) + { + SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); + } + } + private void SetupAxioms() { var axioms = ctx.Axioms; @@ -440,9 +446,8 @@ protected void SendVCOptions() } } - foreach (var entry in options.SmtOptions) { - SendThisVC("(set-option :" + entry.Option + " " + entry.Value + ")"); - } + + SendSolverOptions(); } protected void SendVCId(string descriptiveName) @@ -1172,18 +1177,10 @@ public override void SetRlimit(uint limit) options.ResourceLimit = limit; } - public override void SetLocalSMTOption(string name, string value) - { - options.SmtOptions.Add(new OptionValue(name, value)); - } - - public override void ClearLocalSMTOptions() + public override void SetAdditionalSmtOptions(IEnumerable entries) { - // Go back to global options - options.SmtOptions.Clear(); - options.Parse(libOptions.ProverOptions); + additionalSmtOptions = entries; } - protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown) { var result = Outcome.Undetermined; diff --git a/Source/Provers/SMTLib/SMTLibSolverOptions.cs b/Source/Provers/SMTLib/SMTLibSolverOptions.cs index b7ea04801..379b923d0 100644 --- a/Source/Provers/SMTLib/SMTLibSolverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibSolverOptions.cs @@ -38,13 +38,13 @@ public class SMTLibSolverOptions : ProverOptions public bool UseWeights = true; public bool UseTickleBool => Solver == SolverKind.Z3; public SolverKind Solver = SolverKind.Z3; - public List SmtOptions = new List(); - public List SolverArguments = new List(); + public List SmtOptions = new(); + public List SolverArguments = new(); public string Logic = null; // Z3 specific (at the moment; some of them make sense also for other provers) public string Inspector = null; - + public SMTLibSolverOptions(SMTLibOptions libOptions) : base(libOptions) { } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 81645ed94..a6477eecb 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1353,9 +1353,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa Print(); } - foreach (var entry in Implementation.GetExtraSMTOptions()) { - checker.TheoremProver.SetLocalSMTOption(entry.Key, entry.Value); - } + checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions().Select(kv => new OptionValue(kv.Key, kv.Value))); await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken); } diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index a83a7bf47..bc9cf44d8 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -193,8 +193,6 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch batchCompletions.OnNext((split, result)); await checker.GoBackToIdle(); } - - checker.TheoremProver.ClearLocalSMTOptions(); } private static bool IsProverFailed(ProverInterface.Outcome outcome) From 26dd623cf3354b5fbf1f6c5eb144494b124b2c39 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 20 Nov 2023 15:51:15 +0100 Subject: [PATCH 2/4] Rename --- Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs | 6 +++--- Test/.lit_test_times.txt | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) create mode 100644 Test/.lit_test_times.txt diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs index 5490c52db..d3fd82763 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -347,7 +347,7 @@ protected virtual void PrepareCommon() SendCommon("(set-option :produce-models true)"); } - SendSolverOptions(); + SendSmtOptions(); if (!string.IsNullOrEmpty(options.Logic)) { @@ -391,7 +391,7 @@ protected virtual void PrepareCommon() } } - private void SendSolverOptions() + private void SendSmtOptions() { foreach (var opt in options.SmtOptions.Concat(additionalSmtOptions)) { @@ -447,7 +447,7 @@ protected void SendVCOptions() } - SendSolverOptions(); + SendSmtOptions(); } protected void SendVCId(string descriptiveName) diff --git a/Test/.lit_test_times.txt b/Test/.lit_test_times.txt new file mode 100644 index 000000000..1b094f334 --- /dev/null +++ b/Test/.lit_test_times.txt @@ -0,0 +1 @@ +6.946981e-01 prover/smt-options.bpl From 8661f5c5805a0bdf1486dcc9369ab164860551eb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 20 Nov 2023 16:13:02 +0100 Subject: [PATCH 3/4] Remove build file --- Test/.lit_test_times.txt | 1 - 1 file changed, 1 deletion(-) delete mode 100644 Test/.lit_test_times.txt diff --git a/Test/.lit_test_times.txt b/Test/.lit_test_times.txt deleted file mode 100644 index 1b094f334..000000000 --- a/Test/.lit_test_times.txt +++ /dev/null @@ -1 +0,0 @@ -6.946981e-01 prover/smt-options.bpl From 00a91885fa30aee21e14b65f3b168534428e9ea7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 20 Nov 2023 16:18:15 +0100 Subject: [PATCH 4/4] Fix bad refactoring --- .../SMTLib/SMTLibProcessTheoremProver.cs | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs index d3fd82763..e41e313be 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -1,5 +1,4 @@ using System; -using System.Collections.Concurrent; using System.Collections.Generic; using System.IO; using System.Linq; @@ -8,7 +7,6 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.TypeErasure; using System.Text; -using System.Runtime.CompilerServices; namespace Microsoft.Boogie.SMTLib { @@ -47,7 +45,7 @@ private void ObjectInvariant() } [NotDelayed] - protected SMTLibProcessTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions options, VCExpressionGenerator gen, + public SMTLibProcessTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions options, VCExpressionGenerator gen, SMTLibProverContext ctx) { Contract.Requires(options != null); @@ -347,7 +345,10 @@ protected virtual void PrepareCommon() SendCommon("(set-option :produce-models true)"); } - SendSmtOptions(); + foreach (var opt in SmtOptions()) + { + SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); + } if (!string.IsNullOrEmpty(options.Logic)) { @@ -391,12 +392,9 @@ protected virtual void PrepareCommon() } } - private void SendSmtOptions() + private IEnumerable SmtOptions() { - foreach (var opt in options.SmtOptions.Concat(additionalSmtOptions)) - { - SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); - } + return options.SmtOptions.Concat(additionalSmtOptions); } private void SetupAxioms() @@ -446,8 +444,10 @@ protected void SendVCOptions() } } - - SendSmtOptions(); + foreach (var opt in SmtOptions()) + { + SendThisVC("(set-option :" + opt.Option + " " + opt.Value + ")"); + } } protected void SendVCId(string descriptiveName)