patched two occurrences of StackOverflowException on benchmarks from IronClad

1 files changed, 29 insertions, 6 deletions

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 02220057..c9d4f1c3 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -288,14 +288,15 @@ namespace Microsoft.Boogie.VCExprAST {
            node.Op == VCExpressionGenerator.ImpliesOp)) {

         Contract.Assert(node.Op != null);

         VCExprOp op = node.Op;

-

-        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

-        enumerator.MoveNext();  // skip the node itself

-

+        HashSet<VCExprOp> ops = new HashSet<VCExprOp>();

+        ops.Add(VCExpressionGenerator.AndOp);

+        ops.Add(VCExpressionGenerator.OrOp);

+        ops.Add(VCExpressionGenerator.ImpliesOp);

+        IEnumerator enumerator = new VCExprNAryMultiUniformOpEnumerator(node, ops);

         while (enumerator.MoveNext()) {

-          VCExpr/*!*/ expr = cce.NonNull((VCExpr/*!*/)enumerator.Current);

+          VCExpr expr = cce.NonNull((VCExpr)enumerator.Current);

           VCExprNAry naryExpr = expr as VCExprNAry;

-          if (naryExpr == null || !naryExpr.Op.Equals(op)) {

+          if (naryExpr == null || !ops.Contains(naryExpr.Op)) {

             expr.Accept(this, arg);

           } else {

             StandardResult(expr, arg);

@@ -433,6 +434,28 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

+  public class VCExprNAryMultiUniformOpEnumerator : VCExprNAryEnumerator

+  {

+      private readonly HashSet<VCExprOp> Ops;

+      [ContractInvariantMethod]

+      void ObjectInvariant()

+      {

+          Contract.Invariant(Ops != null);

+      }

+

+      public VCExprNAryMultiUniformOpEnumerator(VCExprNAry completeExpr, HashSet<VCExprOp> ops)

+          : base(completeExpr)

+      {

+          Contract.Requires(completeExpr != null);

+

+          this.Ops = ops;

+      }

+      protected override bool Descend(VCExprNAry expr)

+      {

+          return Ops.Contains(expr.Op) && expr.TypeParamArity == 0;

+      }

+  }

+

   //////////////////////////////////////////////////////////////////////////////

   // Visitor that knows about the variables bound at each location in a VCExpr