Merge branch 'master' of https://github.com/boogie-org/boogie

2 files changed, 26 insertions, 17 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 594f2509..e09eabcb 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -1269,28 +1269,24 @@ namespace Microsoft.Boogie.SMTLib
               SendThisVC("; begin timeout diagnostics");

 

               var unverified = new SortedSet<int>(ctx.TimeoutDiagnosticIDToAssertion.Keys);

-              var lastCnt = unverified.Count + 1;

-              var mod = 2;

+              var lastCnt = 0;

               var timeLimit = options.TimeLimit;

               var timeLimitFactor = 1;

+              var frac = 2;

               while (true)

               {

-                // TODO(wuestholz): Try out different ways for splitting up the work.

-                var split0 = new SortedSet<int>(unverified.Where((val, idx) => idx % mod == 0));

-                var split1 = new SortedSet<int>(unverified.Except(split0));

-

                 int cnt = unverified.Count;

-

                 if (cnt == 0)

                 {

                   result = Outcome.Valid;

                   break;

                 }

-                else if (lastCnt == cnt)

+                

+                if (lastCnt == cnt)

                 {

-                  if (mod < cnt)

+                  if ((2 * frac) < cnt)

                   {

-                    mod++;

+                    frac *= 2;

                   }

                   else if (timeLimitFactor <= 3 && 0 < timeLimit)

                   {

@@ -1312,13 +1308,19 @@ namespace Microsoft.Boogie.SMTLib
                 }

                 else

                 {

-                  mod = 2;

+                  frac = 2;

                 }

                 lastCnt = cnt;

 

+                // TODO(wuestholz): Try out different ways for splitting up the work (e.g., randomly).

+                var cnt0 = cnt / frac;

+                var split0 = new SortedSet<int>(unverified.Where((val, idx) => idx < cnt0));

+                var split1 = new SortedSet<int>(unverified.Except(split0));

+

                 if (0 < split0.Count)

                 {

-                  var result0 = CheckSplit(split0, ref popLater, timeLimitFactor * timeLimit);

+                  var stl = 0 < timeLimit ? split0.Count * ((timeLimit / cnt) + 1) : timeLimit;

+                  var result0 = CheckSplit(split0, ref popLater, timeLimitFactor * stl);

                   if (result0 == Outcome.Valid)

                   {

                     unverified.ExceptWith(split0);

@@ -1332,7 +1334,8 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (0 < split1.Count)

                 {

-                  var result1 = CheckSplit(split1, ref popLater, timeLimitFactor * timeLimit);

+                  var stl = 0 < timeLimit ? split1.Count * ((timeLimit / cnt) + 1) : timeLimit;

+                  var result1 = CheckSplit(split1, ref popLater, timeLimitFactor * stl);

                   if (result1 == Outcome.Valid)

                   {

                     unverified.ExceptWith(split1);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 69b7c8cc..43b5f88a 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -365,13 +365,16 @@ namespace VC {
     public Dictionary<Block, List<CallSite>> callSites;

     public Dictionary<Block, List<CallSite>> recordProcCallSites;

     public bool initialized { get; private set; }

+    // Instrumentation to apply after PassiveImpl, but before VCGen

+    Action<Implementation> PassiveImplInstrumentation;

 

     // boolControlVC (block -> its Bool variable)

     public Dictionary<Block, VCExprVar> blockToControlVar; 

 

-    public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) {

+    public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen, Action<Implementation> PassiveImplInstrumentation) {

       vcgen = stratifiedVcGen;

       impl = implementation;

+      this.PassiveImplInstrumentation = PassiveImplInstrumentation;

 

       List<Variable> functionInterfaceVars = new List<Variable>();

       foreach (Variable v in vcgen.program.GlobalVariables) {

@@ -581,6 +584,9 @@ namespace VC {
       vcgen.ConvertCFG2DAG(impl);

       vcgen.PassifyImpl(impl, out mvInfo);

 

+      if (PassiveImplInstrumentation != null)

+          PassiveImplInstrumentation(impl);

+                

       VCExpressionGenerator gen = proverInterface.VCExprGen;

       var exprGen = proverInterface.Context.ExprGen;

       var translator = proverInterface.Context.BoogieExprTranslator;

@@ -636,12 +642,12 @@ namespace VC {
     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

     public ProverInterface prover;

 

-    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers, Action<Implementation> PassiveImplInstrumentation)

       : base(program, logFilePath, appendLogFile, checkers) {

       implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();

       prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);

       foreach (var impl in program.Implementations) {

-        implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

+        implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this, PassiveImplInstrumentation);

       }

       GenerateRecordFunctions();

     }

@@ -847,7 +853,7 @@ namespace VC {
     }

 

     public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

-      : base(program, logFilePath, appendLogFile, checkers) {

+      : base(program, logFilePath, appendLogFile, checkers, null) {

       PersistCallTree = false;

       procsThatReachedRecBound = new HashSet<string>();

       procsToSkip = new HashSet<string>();