Recursive walking of Exprs doesn't play nice when the depth of the AST is high.

Reduce depth of AST whenever possible (e.g., use a binary tree instead of a
linear list of terms)

5 files changed, 29 insertions, 16 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 792262d3..d8cb623b 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -394,6 +394,23 @@ namespace Microsoft.Boogie {
       args.Add(subexpr);

       return new NAryExpr(x, new TypeCoercion(x, type), args);

     }

+

+    public static Expr BinaryTreeAnd(List<Expr> terms)

+    {

+        return BinaryTreeAnd(terms, 0, terms.Count - 1);

+    }

+

+    private static Expr BinaryTreeAnd(List<Expr> terms, int start, int end)

+    {

+        if (start > end)

+            return Expr.True;

+        if (start == end)

+            return terms[start];

+        if (start + 1 == end)

+            return Expr.And(terms[start], terms[start + 1]);

+        var mid = (start + end) / 2;

+        return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));

+    }

   }

   [ContractClassFor(typeof(Expr))]

   public abstract class ExprContracts : Expr {

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 6817da88..95c29157 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -179,7 +179,7 @@ namespace Microsoft.Boogie.Houdini {
                     }

                     terms.Add(term);

                 }

-                var env = BinaryTreeAnd(terms, 0, terms.Count - 1);

+                var env = Expr.BinaryTreeAnd(terms);

 

                 env.Typecheck(new TypecheckingContext((IErrorSink)null));

                 var envVC = prover.Context.BoogieExprTranslator.Translate(env);

@@ -268,17 +268,6 @@ namespace Microsoft.Boogie.Houdini {
             return overallOutcome;

         }

 

-        private static Expr BinaryTreeAnd(List<Expr> terms, int start, int end)

-        {

-            if (start > end)

-                return Expr.True;

-            if (start == end)

-                return terms[start];

-            if (start + 1 == end)

-                return Expr.And(terms[start], terms[start + 1]);

-            var mid = (start + end) / 2;

-            return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));

-        }

 

         public IEnumerable<Function> GetAssignment()

         {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index e4f63315..13ff6460 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -241,12 +241,12 @@ namespace VC {
     public void GenerateVC() {

       if (initialized) return;

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

-      Expr assertExpr = new LiteralExpr(Token.NoToken, true);

+      List<Expr> assertConjuncts = new List<Expr>();

       foreach (Variable v in impl.OutParams) {

         Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

         outputVariables.Add(c);

         Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

-        assertExpr = Expr.And(assertExpr, eqExpr);

+        assertConjuncts.Add(eqExpr);

       }

       foreach (IdentifierExpr e in impl.Proc.Modifies) {

         if (e.Decl == null) continue;

@@ -254,9 +254,9 @@ namespace VC {
         Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

         outputVariables.Add(c);

         Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

-        assertExpr = Expr.And(assertExpr, eqExpr);

+        assertConjuncts.Add(eqExpr);

       }

-      exitAssertCmd = new AssertCmd(Token.NoToken, Expr.Not(assertExpr));

+      exitAssertCmd = new AssertCmd(Token.NoToken, Expr.Not(Expr.BinaryTreeAnd(assertConjuncts)));

 

       Program program = vcgen.program;

       ProverInterface proverInterface = vcgen.prover;

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index bed39837..27d2be6b 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -513,3 +513,7 @@ Boogie program verifier finished with 0 verified, 1 error
 

 Boogie program verifier finished with 1 verified, 0 errors

 -----

+----- Running regression test large.bpl to test for StackOverflowException

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
index eb5ff634..5e0ab83f 100644
--- a/Test/stratifiedinline/runtest.bat
+++ b/Test/stratifiedinline/runtest.bat
@@ -40,4 +40,7 @@ echo -----
 echo ----- Running regression test bar13.bpl

 %BGEXE% %* /stratifiedInline:1 /vc:i bar13.bpl

 echo -----

+echo ----- Running regression test large.bpl to test for StackOverflowException

+%BGEXE% %* /stratifiedInline:1 /vc:i large.bpl

+echo -----