Update version, and remove race condition (#811)

`ClearLocalSMTOptions()` was called _after_ the checker was released, which leads to a race condition because a new thread may already be using the checker's options while they're still being cleared. Here's an example: https://github.com/dafny-lang/dafny/actions/runs/6930078076/job/18849083894?pr=4773 This PR reduces statefulness of the code, since it no longer clears and reparses `SMTLibProcessTheoremProver.options`. Instead it has a field `IEnumerable<OptionValue> additionalSmtOptions` that can be used to tweak SmtOptions between runs.
boogie-org · Nov 20, 2023 · 7d4d20d · 7d4d20d
1 parent 7be9229
commit 7d4d20d
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 32 deletions.
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.0.6</Version>
+    <Version>3.0.7</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

diff --git 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<OptionValue> entries)
   {
   }
-
-  // Clear options set with SetLocalSMTOption
-  public virtual void ClearLocalSMTOptions()
-  {
-  }
-
+
   public virtual Task<int> GetRCount()
   {
     throw new NotImplementedException();

diff --git 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
 {
@@ -19,6 +17,7 @@ public abstract class SMTLibProcessTheoremProver : ProverInterface
     protected SMTLibProverContext ctx;
     protected VCExpressionGenerator gen;
     protected SMTLibSolverOptions options;
+    protected IEnumerable<OptionValue> additionalSmtOptions = Array.Empty<OptionValue>();
     protected bool usingUnsatCore;
     private string backgroundPredicates;
 
@@ -346,7 +345,7 @@ protected virtual void PrepareCommon()
           SendCommon("(set-option :produce-models true)");
         }
 
-        foreach (var opt in options.SmtOptions)
+        foreach (var opt in SmtOptions())
         {
           SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
         }
@@ -393,6 +392,11 @@ protected virtual void PrepareCommon()
       }
     }
 
+    private IEnumerable<OptionValue> SmtOptions()
+    {
+      return options.SmtOptions.Concat(additionalSmtOptions);
+    }
+
     private void SetupAxioms()
     {
       var axioms = ctx.Axioms;
@@ -440,8 +444,9 @@ protected void SendVCOptions()
         }
       }
 
-      foreach (var entry in options.SmtOptions) {
-        SendThisVC("(set-option :" + entry.Option + " " + entry.Value + ")");
+      foreach (var opt in SmtOptions())
+      {
+        SendThisVC("(set-option :" + opt.Option + " " + opt.Value + ")");
       }
     }
 
@@ -1172,18 +1177,10 @@ public override void SetRlimit(uint limit)
       options.ResourceLimit = limit;
     }
 
-    public override void SetLocalSMTOption(string name, string value)
+    public override void SetAdditionalSmtOptions(IEnumerable<OptionValue> entries)
     {
-      options.SmtOptions.Add(new OptionValue(name, value));
+      additionalSmtOptions = entries;
     }
-
-    public override void ClearLocalSMTOptions()
-    {
-      // Go back to global options
-      options.SmtOptions.Clear();
-      options.Parse(libOptions.ProverOptions);
-    }
-
     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
@@ -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<OptionValue> SmtOptions = new List<OptionValue>();
-    public List<string> SolverArguments = new List<string>();
+    public List<OptionValue> SmtOptions = new();
+    public List<string> 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
@@ -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
@@ -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)