Resolved some issues with data races.

6 files changed, 128 insertions, 95 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 70ce610d..792262d3 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1588,14 +1588,14 @@ namespace Microsoft.Boogie {
         case Opcode.Neq:

           if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) {

             expr.Fun = new BinaryOperator(tok, Opcode.Iff);

-            arg1 = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new List<Expr> { arg1 });

+            var arg1New = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new List<Expr> { arg1 });

 

             // ugly ... there should be some more general approach,

             // e.g., to typecheck the whole expression again

-            arg1.Type = Type.Bool;

-            ((NAryExpr)arg1).TypeParameters = SimpleTypeParamInstantiation.EMPTY;

+            arg1New.Type = Type.Bool;

+            arg1New.TypeParameters = SimpleTypeParamInstantiation.EMPTY;

 

-            expr.Args[1] = arg1;

+            expr.Args[1] = arg1New;

           }

           break;

       }

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index b8ad122f..5274a20b 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -2963,7 +2963,7 @@ Contract.Requires(that != null);
     public override int GetHashCode(List<TypeVariable> boundVariables) {

       //Contract.Requires(boundVariables != null);

       int res = 1637643879 * Decl.GetHashCode();

-      foreach (Type/*!*/ t in Arguments) {

+      foreach (Type/*!*/ t in Arguments.ToArray()) {

         Contract.Assert(t != null);

         res = res * 3 + t.GetHashCode(boundVariables);

       }

@@ -3017,7 +3017,7 @@ Contract.Requires(that != null);
     public override List<TypeVariable>/*!*/ FreeVariables {

       get {

         List<TypeVariable>/*!*/ res = new List<TypeVariable>();

-        foreach (Type/*!*/ t in Arguments) {

+        foreach (Type/*!*/ t in Arguments.ToArray()) {

           Contract.Assert(t != null);

           res.AppendWithoutDups(t.FreeVariables);

         }

@@ -3028,7 +3028,7 @@ Contract.Requires(that != null);
     public override List<TypeProxy/*!*/>/*!*/ FreeProxies {

       get {

         List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*/>();

-        foreach (Type/*!*/ t in Arguments) {

+        foreach (Type/*!*/ t in Arguments.ToArray()) {

           Contract.Assert(t != null);

           AppendWithoutDups(res, t.FreeProxies);

         }

@@ -3359,7 +3359,7 @@ Contract.Assert(var != null);
         boundVariables.Add(var);

       }

 

-      foreach (Type/*!*/ t in Arguments) {

+      foreach (Type/*!*/ t in Arguments.ToArray()) {

         Contract.Assert(t != null);

         res = res * 5 + t.GetHashCode(boundVariables);

       }

@@ -3425,10 +3425,10 @@ Contract.Assert(var != null);
 

     public override List<TypeVariable>/*!*/ FreeVariables {

       get {

-        List<TypeVariable>/*!*/ res = FreeVariablesIn(Arguments);

+        List<TypeVariable>/*!*/ res = FreeVariablesIn(Arguments.ToList());

         Contract.Assert(res != null);

         res.AppendWithoutDups(Result.FreeVariables);

-        foreach (TypeVariable/*!*/ v in TypeParameters) {

+        foreach (TypeVariable/*!*/ v in TypeParameters.ToArray()) {

           Contract.Assert(v != null);

           res.Remove(v);

         }

@@ -3439,7 +3439,7 @@ Contract.Assert(var != null);
     public override List<TypeProxy/*!*/>/*!*/ FreeProxies {

       get {

         List<TypeProxy/*!*/>/*!*/ res = new List<TypeProxy/*!*//*!*/>();

-        foreach (Type/*!*/ t in Arguments) {

+        foreach (Type/*!*/ t in Arguments.ToArray()) {

           Contract.Assert(t != null);

           AppendWithoutDups(res, t.FreeProxies);

         }

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 4a9ca7a3..556676da 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -32,8 +32,11 @@ namespace Microsoft.Boogie {
     public virtual List<Expr> VisitExprSeq(List<Expr> list) {

       Contract.Requires(list != null);

       Contract.Ensures(Contract.Result<List<Expr>>() != null);

-      for (int i = 0, n = list.Count; i < n; i++)

-        list[i] = (Expr)this.Visit(cce.NonNull(list[i]));

+      lock (list)

+      {

+        for (int i = 0, n = list.Count; i < n; i++)

+          list[i] = (Expr)this.Visit(cce.NonNull(list[i]));

+      }

       return list;

     }

   }

@@ -139,8 +142,11 @@ namespace Microsoft.Boogie {
     public virtual List<Block> VisitBlockSeq(List<Block> blockSeq) {

       Contract.Requires(blockSeq != null);

       Contract.Ensures(Contract.Result<List<Block>>() != null);

-      for (int i = 0, n = blockSeq.Count; i < n; i++)

-        blockSeq[i] = this.VisitBlock(cce.NonNull(blockSeq[i]));

+      lock (blockSeq)

+      {

+        for (int i = 0, n = blockSeq.Count; i < n; i++)

+          blockSeq[i] = this.VisitBlock(cce.NonNull(blockSeq[i]));

+      }

       return blockSeq;

     }

     public virtual List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {

@@ -171,8 +177,11 @@ namespace Microsoft.Boogie {
     public virtual List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {

       Contract.Requires(cmdSeq != null);

       Contract.Ensures(Contract.Result<List<Cmd>>() != null);

-      for (int i = 0, n = cmdSeq.Count; i < n; i++)

-        cmdSeq[i] = (Cmd)this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor

+      lock (cmdSeq)

+      {

+        for (int i = 0, n = cmdSeq.Count; i < n; i++)

+          cmdSeq[i] = (Cmd)this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor

+      }

       return cmdSeq;

     }

     public virtual Choice VisitChoice(Choice node) {

@@ -194,8 +203,11 @@ namespace Microsoft.Boogie {
     public virtual CtorType VisitCtorType(CtorType node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<CtorType>() != null);

-      for (int i = 0; i < node.Arguments.Count; ++i)

-        node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

+      lock (node)

+      {

+        for (int i = 0; i < node.Arguments.Count; ++i)

+          node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

+      }

       return node;

     }

     public virtual Declaration VisitDeclaration(Declaration node) {

@@ -321,8 +333,11 @@ namespace Microsoft.Boogie {
     public virtual List<IdentifierExpr> VisitIdentifierExprSeq(List<IdentifierExpr> identifierExprSeq) {

       Contract.Requires(identifierExprSeq != null);

       Contract.Ensures(Contract.Result<List<IdentifierExpr>>() != null);

-      for (int i = 0, n = identifierExprSeq.Count; i < n; i++)

-        identifierExprSeq[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));

+      lock (identifierExprSeq)

+      {

+        for (int i = 0, n = identifierExprSeq.Count; i < n; i++)

+          identifierExprSeq[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));

+      }

       return identifierExprSeq;

     }

     public virtual Implementation VisitImplementation(Implementation node) {

@@ -362,8 +377,11 @@ namespace Microsoft.Boogie {
       //

       // NOTE: when overriding this method, you have to make sure that

       // the bound variables of the map type are updated correctly

-      for (int i = 0; i < node.Arguments.Count; ++i)

-        node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

+      lock (node.Arguments)

+      {

+        for (int i = 0; i < node.Arguments.Count; ++i)

+          node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

+      }

       node.Result = cce.NonNull((Type/*!*/)this.Visit(node.Result));

       return node;

     }

@@ -512,8 +530,11 @@ namespace Microsoft.Boogie {
       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Type>() != null);

       node.ExpandedType = cce.NonNull((Type/*!*/)this.Visit(node.ExpandedType));

-      for (int i = 0; i < node.Arguments.Count; ++i)

-        node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

+      lock (node.Arguments)

+      {

+        for (int i = 0; i < node.Arguments.Count; ++i)

+          node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));

+      }

       return node;

     }

     public virtual Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) {

@@ -549,8 +570,11 @@ namespace Microsoft.Boogie {
     public virtual List<Variable> VisitVariableSeq(List<Variable> variableSeq) {

       Contract.Requires(variableSeq != null);

       Contract.Ensures(Contract.Result<List<Variable>>() != null);

-      for (int i = 0, n = variableSeq.Count; i < n; i++)

-        variableSeq[i] = this.VisitVariable(cce.NonNull(variableSeq[i]));

+      lock (variableSeq)

+      {

+        for (int i = 0, n = variableSeq.Count; i < n; i++)

+          variableSeq[i] = this.VisitVariable(cce.NonNull(variableSeq[i]));

+      }

       return variableSeq;

     }

     public virtual Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 4e94c238..95662d84 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -26,7 +26,7 @@ namespace Microsoft.Boogie.SMTLib
   public class SMTLibProcessTheoremProver : ProverInterface

   {

     private readonly SMTLibProverContext ctx;

-    private readonly VCExpressionGenerator gen;

+    private VCExpressionGenerator gen;

     private readonly SMTLibProverOptions options;

     private bool usingUnsatCore;

     private RPFP rpfp = null;

@@ -396,37 +396,41 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();

     }

 

-    public override void Reset ()

+    public override void Reset(VCExpressionGenerator gen)

     {

-      if (options.Solver == SolverKind.Z3) {

-        SendThisVC ("(reset)");

-		

-	    if (0 < common.Length)

-		{

-          var c = common.ToString ();

-          Process.Send (c);

+      if (options.Solver == SolverKind.Z3)

+      {

+        this.gen = gen;

+        SendThisVC("(reset)");

+

+        if (0 < common.Length)

+        {

+          var c = common.ToString();

+          Process.Send(c);

           if (currentLogFile != null)

-		  {

-            currentLogFile.WriteLine (c);

+          {

+            currentLogFile.WriteLine(c);

           }

         }

       }

     }

-	

-    public override void FullReset ()

+

+    public override void FullReset(VCExpressionGenerator gen)

     {

-      if (options.Solver == SolverKind.Z3) {

-        Namer.Reset ();

-        common.Clear ();

-        SetupAxiomBuilder (gen);

-        Axioms.Clear ();

-        TypeDecls.Clear ();

+      if (options.Solver == SolverKind.Z3)

+      {

+        this.gen = gen;

+        Namer.Reset();

+        common.Clear();

+        SetupAxiomBuilder(gen);

+        Axioms.Clear();

+        TypeDecls.Clear();

         AxiomsAreSetup = false;

-        ctx.Reset ();

-        ctx.KnownDatatypeConstructors.Clear ();

+        ctx.Reset();

+        ctx.KnownDatatypeConstructors.Clear();

         ctx.parent = this;

-        DeclCollector.Reset ();

-        SendThisVC ("; doing a full reset...");

+        DeclCollector.Reset();

+        SendThisVC("; doing a full reset...");

       }

     }

 

@@ -1061,50 +1065,55 @@ namespace Microsoft.Boogie.SMTLib
       Contract.Requires(expr != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      DateTime start = DateTime.UtcNow;

-      //if (CommandLineOptions.Clo.Trace)

-      //  Console.Write("Linearising ... ");

+      lock (gen)

+      {

+        DateTime start = DateTime.UtcNow;

+        //if (CommandLineOptions.Clo.Trace)

+        //  Console.Write("Linearising ... ");

 

-      // handle the types in the VCExpr

-      TypeEraser eraser;

-      switch (CommandLineOptions.Clo.TypeEncodingMethod) {

-        case CommandLineOptions.TypeEncoding.Arguments:

-          eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);

-          break;

-        case CommandLineOptions.TypeEncoding.Monomorphic:

-          eraser = null;

-          break;

-        default:

-          eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);

-          break;

-      }

-      VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity);

-      Contract.Assert(exprWithoutTypes != null);

+        // handle the types in the VCExpr

+        TypeEraser eraser;

+        switch (CommandLineOptions.Clo.TypeEncodingMethod)

+        {

+          case CommandLineOptions.TypeEncoding.Arguments:

+            eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);

+            break;

+          case CommandLineOptions.TypeEncoding.Monomorphic:

+            eraser = null;

+            break;

+          default:

+            eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);

+            break;

+        }

+        VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity);

+        Contract.Assert(exprWithoutTypes != null);

 

-      LetBindingSorter letSorter = new LetBindingSorter(gen);

-      Contract.Assert(letSorter != null);

-      VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true);

-      Contract.Assert(sortedExpr != null);

-      VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);

-      Contract.Assert(sortedAxioms != null);

+        LetBindingSorter letSorter = new LetBindingSorter(gen);

+        Contract.Assert(letSorter != null);

+        VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true);

+        Contract.Assert(sortedExpr != null);

+        VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);

+        Contract.Assert(sortedAxioms != null);

 

-      DeclCollector.Collect(sortedAxioms);

-      DeclCollector.Collect(sortedExpr);

-      FeedTypeDeclsToProver();

+        DeclCollector.Collect(sortedAxioms);

+        DeclCollector.Collect(sortedExpr);

+        FeedTypeDeclsToProver();

 

-      

 

-      AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));

-      string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);

-      Contract.Assert(res != null);

 

-      if (CommandLineOptions.Clo.Trace) {

-        DateTime end = DateTime.UtcNow;

-        TimeSpan elapsed = end - start;

-        if (elapsed.TotalSeconds > 0.5)

-          Console.WriteLine("Linearising   [{0} s]", elapsed.TotalSeconds);

+        AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));

+        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);

+        Contract.Assert(res != null);

+

+        if (CommandLineOptions.Clo.Trace)

+        {

+          DateTime end = DateTime.UtcNow;

+          TimeSpan elapsed = end - start;

+          if (elapsed.TotalSeconds > 0.5)

+            Console.WriteLine("Linearising   [{0} s]", elapsed.TotalSeconds);

+        }

+        return res;

       }

-      return res;

     }

 

     // the list of all known axioms, where have to be included in each

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 3fb0a3ff..0e3cc9d8 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -916,7 +916,7 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Requires(rawType != null);

       Contract.Ensures(Contract.Result<MapType>() != null);

       List<Type>/*!*/ newArguments = new List<Type>();

-      foreach (Type/*!*/ subtype in rawType.Arguments) {

+      foreach (Type/*!*/ subtype in rawType.Arguments.ToList()) {

         Contract.Assert(subtype != null);

         newArguments.Add(ThinOutType(subtype, rawType.TypeParameters,

                                      instantiations));

@@ -964,7 +964,7 @@ namespace Microsoft.Boogie.TypeErasure {
         // traverse the subtypes

         CtorType/*!*/ rawCtorType = rawType.AsCtor;

         List<Type>/*!*/ newArguments = new List<Type>();

-        foreach (Type/*!*/ subtype in rawCtorType.Arguments) {

+        foreach (Type/*!*/ subtype in rawCtorType.Arguments.ToList()) {

           Contract.Assert(subtype != null);

           newArguments.Add(ThinOutType(subtype, boundTypeParams,

                                        instantiations));

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3a8a1af9..62451caa 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -184,7 +184,7 @@ namespace Microsoft.Boogie {
         outcome = default(ProverInterface.Outcome);

         outputExn = default(UnexpectedProverOutputException);

         handler = default(ProverInterface.ErrorHandler);

-        TheoremProver.FullReset();

+        TheoremProver.FullReset(gen);

         ctx.Reset();

         Setup(prog, ctx);

         this.timeout = timeout;

@@ -341,7 +341,7 @@ namespace Microsoft.Boogie {
       outputExn = null;

       this.handler = handler;

 

-      thmProver.Reset();

+      thmProver.Reset(gen);

       SetTimeout();

       proverStart = DateTime.UtcNow;

       thmProver.BeginCheck(descriptiveName, vc, handler);

@@ -494,9 +494,9 @@ namespace Microsoft.Boogie {
     public virtual void Close() {

     }

 

-    public abstract void Reset();

+    public abstract void Reset(VCExpressionGenerator gen);

 

-    public abstract void FullReset();

+    public abstract void FullReset(VCExpressionGenerator gen);

 

     /// <summary>

     /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)

@@ -617,12 +617,12 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

 

-    public override void Reset()

+    public override void Reset(VCExpressionGenerator gen)

     {

       throw new NotImplementedException();

     }

 

-    public override void FullReset()

+    public override void FullReset(VCExpressionGenerator gen)

     {

       throw new NotImplementedException();

     }