Refactored modset analysis to avoid the use of static fields. Static fields cause data races when we run parts of Boogie that both do mod set analysis at the same time.

1 files changed, 11 insertions, 9 deletions

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index c32a921b..7100fc43 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -39,18 +39,23 @@ namespace Microsoft.Boogie {
   }

 

   public class ModSetCollector : ReadOnlyVisitor {

-    static Procedure enclosingProc;

-    static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

-    static HashSet<Procedure> yieldingProcs;

+    private Procedure enclosingProc;

+    private Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

+    private HashSet<Procedure> yieldingProcs;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));

       Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v)));

     }

 

-    static bool moreProcessingRequired;

+    public ModSetCollector() {

+      modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

+      yieldingProcs = new HashSet<Procedure>();

+    }

+

+    private bool moreProcessingRequired;

 

-    public static void DoModSetAnalysis(Program program) {

+    public void DoModSetAnalysis(Program program) {

       Contract.Requires(program != null);

 

       if (CommandLineOptions.Clo.Trace)

@@ -67,9 +72,6 @@ namespace Microsoft.Boogie {
 //          Console.WriteLine("Number of procedures = {0}", procCount);*/

       }

 

-      modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

-      yieldingProcs = new HashSet<Procedure>();

-

       HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();

       foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

         Contract.Assert(decl != null);

@@ -232,7 +234,7 @@ namespace Microsoft.Boogie {
         }

         return ret;

     }

-    private static void ProcessVariable(Variable var) {

+    private void ProcessVariable(Variable var) {

       Procedure/*!*/ localProc = cce.NonNull(enclosingProc);

       if (var == null)

         return;