Handle timeout in refinement loop

1 files changed, 59 insertions, 32 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index fcd126e4..f87e6e51 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -902,6 +902,17 @@ namespace VC {
       }

     }

 

+    class FindLeastOORException : Exception

+    {

+        public Outcome outcome;

+

+        public FindLeastOORException(string msg, Outcome outcome)

+            : base(msg)

+        {

+            this.outcome = outcome;

+        }

+    }

+

     public override Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

@@ -930,45 +941,58 @@ namespace VC {
       calls.setCurrProcAsMain();

       vcMain = calls.Mutate(vcMain, true);

 

-      // Put all of the necessary state into one object

-      var vState = new VerificationState(vcMain, calls, prover, new EmptyErrorHandler());

+      try

+      {

 

-      // We'll restore the original state of the theorem prover at the end

-      // of this procedure

-      vState.checker.prover.Push();

+          // Put all of the necessary state into one object

+          var vState = new VerificationState(vcMain, calls, prover, new EmptyErrorHandler());

 

-      // Do eager inlining

-      while (calls.currCandidates.Count > 0) {

-        List<int> toExpand = new List<int>();

+          // We'll restore the original state of the theorem prover at the end

+          // of this procedure

+          vState.checker.prover.Push();

 

-        foreach (int id in calls.currCandidates) {

-          Debug.Assert(calls.getRecursionBound(id) <= 1, "Recursion not supported");

-          toExpand.Add(id);

-        }

-        DoExpansion(toExpand, vState);

-      }

+          // Do eager inlining

+          while (calls.currCandidates.Count > 0)

+          {

+              List<int> toExpand = new List<int>();

 

-      // Find all the boolean constants

-      var allConsts = new HashSet<VCExprVar>();

-      foreach (var constant in program.Constants) {

-        if (!allBoolVars.Contains(constant.Name)) continue;

-        var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);

-        allConsts.Add(v);

-      }

+              foreach (int id in calls.currCandidates)

+              {

+                  Debug.Assert(calls.getRecursionBound(id) <= 1, "Recursion not supported");

+                  toExpand.Add(id);

+              }

+              DoExpansion(toExpand, vState);

+          }

 

-      // Now, lets start the algo

-      var min = refinementLoop(vState.checker, new HashSet<VCExprVar>(), allConsts, allConsts);

+          // Find all the boolean constants

+          var allConsts = new HashSet<VCExprVar>();

+          foreach (var constant in program.Constants)

+          {

+              if (!allBoolVars.Contains(constant.Name)) continue;

+              var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);

+              allConsts.Add(v);

+          }

 

-      var ret = new HashSet<string>();

-      foreach (var v in min) {

-        //Console.WriteLine(v.Name);

-        ret.Add(v.Name);

-      }

-      allBoolVars = ret;

+          // Now, lets start the algo

+          var min = refinementLoop(vState.checker, new HashSet<VCExprVar>(), allConsts, allConsts);

 

-      vState.checker.prover.Pop();

+          var ret = new HashSet<string>();

+          foreach (var v in min)

+          {

+              //Console.WriteLine(v.Name);

+              ret.Add(v.Name);

+          }

+          allBoolVars = ret;

 

-      return Outcome.Correct;

+          vState.checker.prover.Pop();

+

+          return Outcome.Correct;

+      }

+      catch (FindLeastOORException e)

+      {

+          Console.WriteLine("Exception in FindLeastToVerify: {0}, {1}", e.Message, e.outcome);

+          return e.outcome;

+      }

     }

 

     private HashSet<VCExprVar> refinementLoop(ApiChecker apiChecker, HashSet<VCExprVar> trackedVars, HashSet<VCExprVar> trackedVarsUpperBound, HashSet<VCExprVar> allVars) {

@@ -1038,7 +1062,10 @@ namespace VC {
       }

 

       var o = apiChecker.CheckAssumptions(assumptions);

-      Debug.Assert(o == Outcome.Correct || o == Outcome.Errors);

+      if (o != Outcome.Correct && o != Outcome.Errors)

+      {

+          throw new FindLeastOORException("OOR", o);

+      }

       //Console.WriteLine("Result = " + o.ToString());

       prover.LogComment("FindLeast: Query End");