Worked on the parallelization.

8 files changed, 46 insertions, 44 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 036c8b66..0874541b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -355,9 +355,7 @@ namespace Microsoft.Boogie
     public static ErrorInformationFactory errorInformationFactory = new ErrorInformationFactory();

 

     public readonly static VerificationResultCache Cache = new VerificationResultCache();

-

-    static LinearTypechecker linearTypechecker;

-

+    

     static List<Checker> Checkers = new List<Checker>();

 

     static IDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

@@ -419,7 +417,8 @@ namespace Microsoft.Boogie
           PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

         }

 

-        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);

+        LinearTypechecker linearTypechecker;

+        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypechecker);

         if (oc != PipelineOutcome.ResolvedAndTypeChecked)

           return;

 

@@ -587,10 +586,13 @@ namespace Microsoft.Boogie
     ///  - TypeCheckingError if a type checking error occurred

     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

     /// </summary>

-    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName)

+    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypechecker linearTypechecker)

     {

       Contract.Requires(program != null);

       Contract.Requires(bplFileName != null);

+

+      linearTypechecker = null;

+

       // ---------- Resolve ------------------------------------------------------------

 

       if (CommandLineOptions.Clo.NoResolve)

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index b5775424..a64cece0 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -134,7 +134,7 @@ namespace Microsoft.Boogie.Houdini {
 

       vcgen.ConvertCFG2DAG(impl);

       ModelViewInfo mvInfo;

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);

+      var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);

 

       ExistentialConstantCollector ecollector;

       ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out ecollector);

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index a1c24fad..ee955def 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -423,7 +423,7 @@ namespace Microsoft.Boogie.SMTLib
       Axioms.Clear();

       TypeDecls.Clear();

       AxiomsAreSetup = false;

-      ctx.Clear();

+      ctx.Reset();

       ctx.KnownDatatypeConstructors.Clear();

       ctx.parent = this;

       DeclCollector.Reset();

diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index ac6ea33a..a46105f8 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -33,15 +33,13 @@ namespace Microsoft.Boogie.VCExprAST {
 

     private UniqueNamer(UniqueNamer namer) {

       Contract.Requires(namer != null);

+

       Spacer = namer.Spacer;

       GlobalNames = new Dictionary<Object, string>(namer.GlobalNames);

-

-      List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ localNames =

-        new List<IDictionary<Object, string>>();

-      LocalNames = localNames;

+      LocalNames = new List<IDictionary<Object, string>>();

 

       foreach (IDictionary<Object/*!*/, string/*!*/>/*!*/ d in namer.LocalNames)

-        localNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));

+        LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));

 

       UsedNames = new HashSet<string>(namer.UsedNames);

       CurrentCounters = new Dictionary<string, int>(namer.CurrentCounters);

@@ -57,6 +55,7 @@ namespace Microsoft.Boogie.VCExprAST {
     {

       GlobalNames.Clear();

       LocalNames.Clear();

+      LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>());

       UsedNames.Clear();

       CurrentCounters.Clear();

       GlobalPlusLocalNames.Clear();

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 1e588760..88e760c7 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -179,7 +179,7 @@ namespace Microsoft.Boogie {
     public void Retarget(Program prog, ProverContext ctx, int timeout = 0)

     {

         TheoremProver.FullReset();

-        ctx.Clear();

+        ctx.Reset();

         Setup(prog, ctx);

         this.timeout = timeout;

         SetTimeout();

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index d8af86e4..5bc5eba3 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1695,10 +1695,14 @@ namespace VC {
       Contract.Requires(impl != null);

 

       // global variables

-      foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>()) {

-        if (!(v is Constant))

+      lock (program.TopLevelDeclarations)

+      {

+        foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>())

         {

-          AllVariables.Add(v);

+          if (!(v is Constant))

+          {

+            AllVariables.Add(v);

+          }

         }

       }

       // implementation parameters

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index a836b6fb..7931a042 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -34,7 +34,7 @@ namespace Microsoft.Boogie
     public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }

     public abstract VCGenerationOptions VCGenOptions { get; }

     public abstract object Clone();

-    public abstract void Clear();

+    public abstract void Reset();

   }

   

 [ContractClassFor(typeof(ProverContext))]

@@ -121,11 +121,11 @@ public abstract class ProverContextContracts:ProverContext{
       this.orderingAxiomBuilder = oab;

     }

 

-    public override void Clear()

+    public override void Reset()

     {

-        SetupOrderingAxiomBuilder(gen, translator);

-        distincts = new List<Variable>();

-        axiomConjuncts = new List<VCExpr>();

+      SetupOrderingAxiomBuilder(gen, translator);

+      distincts = new List<Variable>();

+      axiomConjuncts = new List<VCExpr>();

     }

 

     protected DeclFreeProverContext(DeclFreeProverContext ctxt) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 48b73bce..3d64e790 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -66,7 +66,6 @@ namespace VC {
         Contract.Invariant(parent != null);

         Contract.Invariant(impl != null);

         Contract.Invariant(initial != null);

-        Contract.Invariant(program != null);

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

         Contract.Invariant(cce.NonNull(visited));

         Contract.Invariant(callback != null);

@@ -75,21 +74,18 @@ namespace VC {
       VCGen parent;

       Implementation impl;

       Block initial;

-      Program program;

       int id;

       Dictionary<Block, Block> copies = new Dictionary<Block, Block>();

       HashSet<Block> visited = new HashSet<Block>();

       VerifierCallback callback;

 

-      internal SmokeTester(VCGen par, Implementation i, Program prog, VerifierCallback callback) {

+      internal SmokeTester(VCGen par, Implementation i, VerifierCallback callback) {

         Contract.Requires(par != null);

         Contract.Requires(i != null);

-        Contract.Requires(prog != null);

         Contract.Requires(callback != null);

         parent = par;

         impl = i;

         initial = i.Blocks[0];

-        program = prog;

         this.callback = callback;

       }

 

@@ -1196,8 +1192,7 @@ namespace VC {
         checker = parent.FindCheckerFor(timeout);

         Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();

 

-        ProverInterface tp = checker.TheoremProver;

-        ProverContext ctx = tp.Context;

+        ProverContext ctx = checker.TheoremProver.Context;

         Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;

         bet.SetCodeExprConverter(

           new CodeExprConverter(

@@ -1407,16 +1402,12 @@ namespace VC {
 

       SmokeTester smoke_tester = null;

       if (CommandLineOptions.Clo.SoundnessSmokeTest) {

-        smoke_tester = new SmokeTester(this, impl, program, callback);

+        smoke_tester = new SmokeTester(this, impl, callback);

         smoke_tester.Copy();

       }

 

       ModelViewInfo mvInfo;

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

-      lock (program)

-      {

-        gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

-      }

+      var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

 

       double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;

       int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits, 

@@ -1661,7 +1652,7 @@ namespace VC {
         Contract.Assert(traceNodes.Contains(entryBlock));

         trace.Add(entryBlock);

 

-        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, model, MvInfo, incarnationOriginMap, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());

+        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, model, MvInfo, incarnationOriginMap, context, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());

 

         if (newCounterexample == null)

           return;

@@ -2039,11 +2030,15 @@ namespace VC {
       {

         CmdSeq cc = new CmdSeq();

         // where clauses of global variables

-        foreach (Declaration d in program.TopLevelDeclarations) {

-          GlobalVariable gvar = d as GlobalVariable;

-          if (gvar != null && gvar.TypedIdent.WhereExpr != null) {

-            Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);

-            cc.Add(c);

+        lock (program.TopLevelDeclarations)

+        {

+          foreach (var gvar in program.TopLevelDeclarations.OfType<GlobalVariable>())

+          {

+            if (gvar != null && gvar.TypedIdent.WhereExpr != null)

+            {

+              Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);

+              cc.Add(c);

+            }

           }

         }

         // where clauses of in- and out-parameters

@@ -2118,7 +2113,10 @@ namespace VC {
         List<Expr> axioms;

         List<Function> functions;

         LambdaHelper.Desugar(impl, out axioms, out functions);

-        program.TopLevelDeclarations.AddRange(functions);

+        lock (program.TopLevelDeclarations)

+        {

+          program.TopLevelDeclarations.AddRange(functions);

+        }

 

         if (axioms.Count > 0) {

           CmdSeq cmds = new CmdSeq();

@@ -2364,7 +2362,7 @@ namespace VC {
     static Counterexample TraceCounterexample(

                           Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, Model errModel, ModelViewInfo mvInfo,

                           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

-                          ProverContext/*!*/ context, Program/*!*/ program,

+                          ProverContext/*!*/ context,

                           Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)

     {

       Contract.Requires(b != null);

@@ -2372,7 +2370,6 @@ namespace VC {
       Contract.Requires(trace != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));

       Contract.Requires(context != null);

-      Contract.Requires(program != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));

       // After translation, all potential errors come from asserts.

       CmdSeq cmds = b.Cmds;

@@ -2400,7 +2397,7 @@ namespace VC {
           Contract.Assert(bb != null);

           if (traceNodes.Contains(bb)){

             trace.Add(bb);

-            return TraceCounterexample(bb, traceNodes, trace, errModel, mvInfo, incarnationOriginMap, context, program, calleeCounterexamples);

+            return TraceCounterexample(bb, traceNodes, trace, errModel, mvInfo, incarnationOriginMap, context, calleeCounterexamples);

           }

         }

       }