changes to support a configured errorLimit

8 files changed, 42 insertions, 28 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 5f60d93e..dd512c96 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -398,7 +398,6 @@ namespace Microsoft.Boogie {
     public bool ContractInfer = false;

     public bool ExplainHoudini = false;

     public bool ConcurrentHoudini = false;

-    public bool DisableLoopInvMaintainedAssert = false;

     public bool ModifyTopologicalSorting = false;

     public bool DebugParallelHoudini = false;

     public bool HoudiniUseCrossDependencies = false;

@@ -649,10 +648,10 @@ namespace Microsoft.Boogie {
 

     public class ConcurrentHoudiniOptions

     {

+      public List<string> ProverOptions = new List<string>();

       public int ProverCCLimit = 5;

       public bool DisableLoopInvMaintainedAssert = false;

       public bool ModifyTopologicalSorting = false;

-      public int LoopUnrollCount = -1;

     }

     public List<ConcurrentHoudiniOptions> Cho = new List<ConcurrentHoudiniOptions>();

 

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 30d6062f..252321b6 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -130,13 +130,13 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

-    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int houdiniID = -1) {

+    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int taskID = -1) {

       this.descriptiveName = impl.Name;

       this.stats = stats;

       collector = new ConditionGeneration.CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

 

-      vcgen.ConvertCFG2DAG(impl, threadID: houdiniID);

+      vcgen.ConvertCFG2DAG(impl, taskID: taskID);

       ModelViewInfo mvInfo;

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

 

@@ -222,7 +222,7 @@ namespace Microsoft.Boogie.Houdini {
       return expr;

     }

 

-    public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {

+    public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors, int taskID = -1) {

       collector.examples.Clear();

 

       if (CommandLineOptions.Clo.Trace) {

@@ -232,7 +232,7 @@ namespace Microsoft.Boogie.Houdini {
 

       VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);

       proverInterface.BeginCheck(descriptiveName, vc, handler);

-      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);

+      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, taskID: taskID);

 

       double queryTime = (DateTime.UtcNow - now).TotalSeconds;

       stats.proverTime += queryTime;

diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index a75cc054..f4bab257 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -43,7 +43,7 @@ namespace Microsoft.Boogie.Houdini
       Inline();
 
       this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, id);
 
       vcgenFailures = new HashSet<Implementation>();
       Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
@@ -53,7 +53,7 @@ namespace Microsoft.Boogie.Houdini
         try {
           if (CommandLineOptions.Clo.Trace)
             Console.WriteLine("Generating VC for {0}", impl.Name);
-          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, id);
+          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: id);
           houdiniSessions.Add(impl, session);
         }
         catch (VCGenException) {
@@ -260,5 +260,18 @@ namespace Microsoft.Boogie.Houdini
         }
       } 
     }
+
+    protected override ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
+      ProverInterface.Outcome outcome;
+      try {
+        outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors, taskID: id);
+      }
+      catch (UnexpectedProverOutputException upo) {
+        Contract.Assume(upo != null);
+        errors = null;
+        outcome = ProverInterface.Outcome.Undetermined;
+      }
+      return outcome;
+    }
   }
 }
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 12c972f3..c3575800 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -1086,7 +1086,7 @@ namespace Microsoft.Boogie.Houdini {
       return null;

     }

 

-    protected ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {

+    protected virtual ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {

       ProverInterface.Outcome outcome;

       try {

         outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors);

@@ -1099,7 +1099,7 @@ namespace Microsoft.Boogie.Houdini {
       return outcome;

     }

 

-    private Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

+    protected Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

     {

       Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);

       foreach (var c in program.TopLevelDeclarations.OfType<Constant>())

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 95662d84..4a5d23d6 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -793,11 +793,11 @@ namespace Microsoft.Boogie.SMTLib
     }

 

     [NoDefaultContract]

-    public override Outcome CheckOutcome(ErrorHandler handler)

+    public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1)

     {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

-      var result = CheckOutcomeCore(handler);

+      var result = CheckOutcomeCore(handler, taskID: taskID);

       SendThisVC("(pop 1)");

       FlushLogFile();

 

@@ -805,7 +805,7 @@ namespace Microsoft.Boogie.SMTLib
     }

 

     [NoDefaultContract]

-    public override Outcome CheckOutcomeCore(ErrorHandler handler)

+    public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)

     {  

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       

@@ -819,6 +819,10 @@ namespace Microsoft.Boogie.SMTLib
         FlushProverWarnings();

 

         var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;

+        if (taskID >= 0) {

+          errorsLeft = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit;

+        }

+

         if (errorsLeft < 1)

           errorsLeft = 1;

 

@@ -1314,7 +1318,7 @@ namespace Microsoft.Boogie.SMTLib
             i++;

         }

         Check();

-

+        

         var outcome = CheckOutcomeCore(handler);

 

         if (outcome != Outcome.Valid) {

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 2237c2fc..549c700a 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -378,7 +378,7 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------

 

   public abstract class ProverInterface {

-    public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {

+    public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {

       Contract.Requires(prog != null);

 

       ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();

@@ -393,7 +393,11 @@ namespace Microsoft.Boogie {
         options.TimeLimit = timeout * 1000;

       }

 

-      options.Parse(CommandLineOptions.Clo.ProverOptions);

+      if (taskID >= 0) {

+        options.Parse(CommandLineOptions.Clo.Cho[taskID].ProverOptions);

+      } else {

+        options.Parse(CommandLineOptions.Clo.ProverOptions);

+      }

 

       ProverContext ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

 

@@ -492,7 +496,7 @@ namespace Microsoft.Boogie {
         throw new System.NotImplementedException();

     }

     [NoDefaultContract]

-    public abstract Outcome CheckOutcome(ErrorHandler handler);

+    public abstract Outcome CheckOutcome(ErrorHandler handler, int taskID = -1);

     public virtual string[] CalculatePath(int controlFlowConstant) {

       throw new System.NotImplementedException();

     }

@@ -560,7 +564,7 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

 

-    public virtual Outcome CheckOutcomeCore(ErrorHandler handler)

+    public virtual Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)

     {

         throw new NotImplementedException();

     }

@@ -619,7 +623,7 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

     [NoDefaultContract]

-    public override Outcome CheckOutcome(ErrorHandler handler) {

+    public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) {

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

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index ceea2477..7d8d749c 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1073,6 +1073,7 @@ namespace VC {
       private Outcome CheckVC() {

         prover.Check();

         ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);

+

         return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);

       }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 5880eb16..e02f96d5 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1875,7 +1875,7 @@ namespace VC {
           }

       }

 

-    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null, int threadID = -1)

+    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null, int taskID = -1)

     {

     Contract.Requires(impl != null);

       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

@@ -1946,7 +1946,7 @@ namespace VC {
               prefixOfPredicateCmdsInit.Add(b);

 

               if (CommandLineOptions.Clo.ConcurrentHoudini) {

-                if (CommandLineOptions.Clo.Cho[threadID].DisableLoopInvMaintainedAssert)

+                if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvMaintainedAssert)

                   b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);

                 else

                   b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

@@ -1954,13 +1954,6 @@ namespace VC {
                 b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

               }

 

-              if (threadID >= 0 && CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)

-

-              if (CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)

-                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);

-              else

-                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

-

               b.Attributes = c.Attributes; 

               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsMaintained.Add(b);